Context-Dependent Effects and Concurrency in Guarded Interaction Trees

TL;DR

<3-5 sentence high-level summary> Guarded Interaction Trees extend the ITrees framework to support higher‑order and context‑dependent effects within Rocq, enabling direct‑style semantics for control operators such as call/cc and delimited continuations. The paper develops a conservative, modular extension to the program logic and semantics, introduces context‑dependent reifiers, and proves adequacy and type‑soundness via logical relations. It also demonstrates modeling of exceptions and delimited continuations, and shows how to compose these effects with higher‑order store to enable safe interoperability between languages; an orthogonal preemptive concurrency extension with atomic state modification further showcases modular reasoning. Together, these results advance scalable, modular reasoning about complex language features in Rocq using GITrees and Iris. The work also discusses connections to prior work on extensible denotational semantics and provides avenues for future exploration in handlers, concurrency, and more general effect interactions.

Abstract

Guarded Interaction Trees are a structure and a fully formalized framework for representing higher-order computations with higher-order effects in Rocq. We present an extension of Guarded Interaction Trees to support formal reasoning about context-dependent effects. That is, effects whose behaviors depend on the evaluation context, e.g., call/cc, shift and reset. Using and reasoning about such effects is challenging since certain compositionality principles no longer hold in the presence of such effects. For example, the so-called ``bind rule'' in modern program logics is no longer valid. The goal of our extension is to support representation and reasoning about context-dependent effects in the most painless way possible. To that end, our extension is conservative: the reasoning principles for context-independent effects remain the same. We use it to give direct-style denotational semantics for higher-order programming languages with call/cc and with delimited continuations. We extend the program logic for Guarded Interaction Trees to account for context-dependent effects, and we use the program logic to prove that the denotational semantics is adequate with respect to the operational semantics. Additionally, we retain the ability to combine multiple effects in a modular way, which we demonstrate by showing type soundness for safe interoperability of a programming language with delimited continuations and a programming language with higher-order store. Furthermore, as another contribution, in addition to context-dependent effects, we show how to extend Guarded Interaction Trees with preemptive concurrency. To support implementation and verification of concurrent data structures and algorithms in the presence of preemptive concurrency one requires atomic state modification operations, e.g., compare-and-exchange.

Figures (30)

• Figure 1: Grammar for the Iris base logic.
• Figure 2: Guarded datatype of interaction trees.
• Figure 3: Example function on Guarded Interaction Trees.
• Figure 4: Signature of reifiers and the reification function
• Figure 5: Selected weakest precondition rules.

Theorems & Definitions (20)

• definition 1: Homomorphism
• lemma 1
• theorem 1
• lemma 2
• lemma 3
• lemma 4
• lemma 5
• lemma 6
• proof : of \ref{['lem:cc:adequacy']}
• theorem 2: Soundness