Write a Blog >>

Interaction trees (ITrees) are a general-purpose data structure in Coq for representing the behaviors of recursive programs that interact with their environments. ITrees, a coinductive variant of "free monads,'' 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. And 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 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, which mechanizes classic domain- and category-theoretic results about program semantics, iteration, monadic structures, and equational reasoning. Although the internals of the library make heavy use of 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 demonstrate 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 as ITree-based denotational semantics. Unlike previous results using operational techniques, this bisimulation proof follows straightforwardly by structural induction and elementary rewriting via an equational theory of combinators for control-flow graphs.

Interaction Trees (LibreOffice slides, with animations) (itrees-popl20.odp)233KiB
Interaction Trees (PDF slides) (itrees-popl20.pdf)242KiB

Fri 24 Jan
Times are displayed in time zone: Saskatchewan, Central America change

10:30 - 11:35: Verification in Proof AssistantsResearch Papers at Ile de France III (IDF III)
Chair(s): Sandrine BlazyUniv Rennes- IRISA
10:30 - 10:51
Virtual Timeline: A Formal Abstraction for Verifying Preemptive Schedulers with Temporal Isolation
Research Papers
Mengqi LiuYale University, Lionel RiegVerimag, Zhong ShaoYale University, Ronghui GuColumbia University, David CostanzoYale University, Jung-Eun KimYale University, Man-Ki YoonYale University
Link to publication DOI Media Attached File Attached
10:51 - 11:13
The High-Level Benefits of Low-Level Sandboxing
Research Papers
Michael SammlerMPI-SWS, Deepak GargMax Planck Institute for Software Systems, Derek DreyerMPI-SWS, Tadeusz LitakFAU Erlangen-Nuremberg, INF 8
Link to publication DOI Media Attached
11:13 - 11:35
Interaction Trees: Representing Recursive and Impure Programs in CoqDistinguished Paper
Research Papers
Li-yao XiaUniversity of Pennsylvania, Yannick ZakowskiUniversity of Pennsylvania, Paul HeUniversity of Pennsylvania, Chung-Kil HurSeoul National University, Gregory MalechaBedRock Systems, Benjamin C. PierceUniversity of Pennsylvania, Steve ZdancewicUniversity of Pennsylvania
Link to publication DOI Media Attached File Attached