Modular Denotational Semantics for Effects with Guarded Interaction Trees
- Distinguished paper award
Journal Paper
We present guarded interaction trees — a structure and a fully formalized framework for representing higher-order computations with higher-order effects in Coq, inspired by domain theory and the recently proposed interaction trees. We also present an accompanying separation logic for reasoning about guarded interaction trees. To demonstrate that guarded interaction trees provide a convenient domain for interpreting higher-order languages with effects, we define an interpretation of a PCF-like language with effects and show that this interpretation is sound and computationally adequate; we prove the latter using a logical relation defined using the separation logic. Guarded interaction trees also allow us to combine different effects and reason about them modularly. To illustrate this point, we give a modular proof of type soundness of cross-language interactions for safe interoperability of different higher-order languages with different effects. All results in the paper are formalized in Coq using the Iris logic over guarded type theory.
The bibtex source for this publication:
@article{DBLP:journals/pacmpl/FruminTB24,
author = {Dan Frumin and
Amin Timany and
Lars Birkedal},
title = {Modular Denotational Semantics for Effects with Guarded Interaction
Trees},
journal = {Proc. {ACM} Program. Lang.},
volume = {8},
number = {{POPL}},
pages = {332--361},
year = {2024},
url = {https://doi.org/10.1145/3632854},
doi = {10.1145/3632854},
timestamp = {Mon, 05 Feb 2024 20:23:03 +0100},
biburl = {https://dblp.org/rec/journals/pacmpl/FruminTB24.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}