Interaction Trees: Representing Recursive and Impure Programs in Coq

TL;DR

Interaction trees (ITrees) are a versatile coinductive data structure in Coq for modeling recursive, impure, and nonterminating programs with formal semantics, enabling executable interpreters and verified compilers.

Contribution

The paper introduces ITrees as a new coinductive structure for representing complex program behaviors, along with a Coq library and a verified compiler correctness proof.

Findings

ITrees can represent nonterminating, impure recursive computations.

The Coq library mechanizes key semantic theories and supports reasoning.

A verified compiler from a simple language to assembly is demonstrated.

Abstract

"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.