# Interaction Trees: Representing Recursive and Impure Programs in Coq

arXiv: https://arxiv.org/abs/1906.00046 · HTML: https://mlsanity.com/paper/1906.00046/

## Key facts

- Cited by 7 papers in the map (data through 14 Oct 2026).
- First posted on arXiv 31 May 2019.

## Built on by (most cited first, 7 of 7)

- [Shepherd: Enabling Programmable Meta-Agents via Reversible Agentic Execution Traces](https://mlsanity.com/paper/2605.10913/) (2026)
- [Mechanized Foundations of Structural Governance: Machine-Checked Proofs for Governed Intelligence](https://mlsanity.com/paper/2604.27289/) (2026)
- [A Case Study on the Effectiveness of LLMs in Verification with Proof Assistants](https://mlsanity.com/paper/2508.18587/) (2025)
- [Effect-Transparent Governance for AI Workflow Architectures: Semantic Preservation, Expressive Minimality, and Decidability Boundaries](https://mlsanity.com/paper/2605.01030/) (2026)
- [Algebraic Semantics of Governed Execution: Monoidal Categories, Effect Algebras, and Coterminous Boundaries](https://mlsanity.com/paper/2605.01032/) (2026)
- [Governed Metaprogramming for Intelligent Systems: Reclassifying Eval as a Governed Effect](https://mlsanity.com/paper/2605.05248/) (2026)
- [Volition Elicitation: Operational Semantics for People and Their Machines](https://mlsanity.com/paper/2607.14138/) (2026)

## Abstract (arXiv)

"Interaction trees" (ITrees) are a general-purpose data structure for representing the behaviors of recursive programs that interact with their environments. A coinductive variant of "free monads," ITrees are built out of uninterpreted events and their continuations. They support compositional construction of interpreters from "event handlers", which give meaning to events by defining their semantics as monadic actions. ITrees are expressive enough to represent impure and potentially nonterminating, mutually recursive computations, while admitting a rich equational theory of equivalence up to weak bisimulation. In contrast to other approaches such as relationally specified operational semantics, ITrees are executable via code extraction, making them suitable for debugging, testing, and implementing software artifacts that are amenable to formal verification. We have implemented ITrees and their associated theory as a Coq library, mechanizing classic domain- and category-theoretic results about program semantics, iteration, monadic structures, and equational reasoning. Although the internals of the library rely heavily on coinductive proofs, the interface hides these details so that clients can use and reason about ITrees without explicit use of Coq's coinduction tactics. To showcase the utility of our theory, we prove the termination-sensitive correctness of a compiler from a simple imperative source language to an assembly-like target whose meanings are given in an ITree-based denotational semantics. Unlike previous results using operational techniques, our bisimulation proof follows straightforwardly by structural induction and elementary rewriting via an equational theory of combinators for control-flow graphs.