We will present the design and implementation of Interaction Trees (ITrees), a general-purpose data-structure for representing in Coq potentially divergent, effectful, programs. 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. They are expressive enough to represent impure and potentially nonterminating, mutually recursive computations in Coq. Finally, they give rise to a theory enabling equational reasoning, up to weak bisimulation, about ITrees and monadic computations built from them. In contrast to other approaches, ITrees are executable via code extraction.

ITrees are expressive enough to serve as a language of specification for many projects of the DeepSpec ecosystem, making them a convenient Franca Lingua for formal specification, and helping in connecting projects together. Furthermore, their ability to be extracted make them compatible with ambitions of liveness and two-sidedness.

In this talk, we will particularly focus on how ITrees can be used in the context of verified compilation. To this end, we will first introduce the core concepts over a toy language, before sketching how we have been scaling the approach to LLVM IR as part of the Vellvm DeepSpec project.