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

Displayed time zone: Pacific Time (US & Canada) change

09:00 - 11:00
REMS-DeepSpec Session 6REMS-DeepSpec at REMS/DeepSpec live stream
Representing recursive and impure programs in Coq: from a toy assembly language to a modular formal semantics for LLVM IR
Yannick Zakowski University of Pennsylvania
The Verified IoT Lightbulb: Connecting Hardware and Software in a Simple Embedded System
Adam Chlipala Massachusetts Institute of Technology, Andres Erbsen , Samuel Gruetter Massachusetts Institute of Technology, Joonwon Choi Massachusetts Institute of Technology, USA