Modular Denotational Semantics for Effects with Guarded Interaction Trees
summary
Introduces guarded interaction trees as a denotational domain for higher-order effects, fully formalized in Coq/Iris formalization with reusable artifacts; proves soundness and computational adequacy of a PCF-like interpretation via a logical relation built in the separation logic; shows handlers-as-state reifiers that execute effects (higher-order store modeled as maps to later trees); delivers a modular proof of type soundness for cross-language interaction and limits runtime errors to a provable linearity exception class.
AI-written summary · about