Write a Blog >>
PLDI 2020
Mon 15 - Fri 19 June 2020
Tue 16 Jun 2020 09:00 - 09:40 at REMS/DeepSpec live stream - REMS-DeepSpec Session 6

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.

Tue 16 Jun
Times are displayed in time zone: (GMT-07:00) Pacific Time (US & Canada) change

09:00 - 11:00: REMS-DeepSpec 2020 - REMS-DeepSpec Session 6 at REMS/DeepSpec live stream
rems-deepspec-202009:00 - 09:40
Yannick ZakowskiUniversity of Pennsylvania
rems-deepspec-202009:50 - 10:30
Adam ChlipalaMassachusetts Institute of Technology, Andres Erbsen, Sam GruetterMassachusetts Institute of Technology, Joonwon ChoiMassachusetts Institute of Technology, USA