Modular Denotational Semantics for Effects with Guarded Interaction Trees

TL;DR

This paper introduces guarded interaction trees in Coq, providing a formal framework for higher-order effects, along with a separation logic, enabling modular reasoning and sound interpretation of effectful languages.

Contribution

It presents guarded interaction trees and a separation logic, offering a formal, modular approach to reasoning about higher-order effects in programming languages.

Findings

Formalization of guarded interaction trees in Coq.

Sound and adequate interpretation of a PCF-like language with effects.

Modular proof of type soundness for cross-language effect interactions.

Abstract

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.