Sat 22 Jun 2019 16:00 - 16:20 at 106B - Interaction Trees and Algebraic Effects I Chair(s): Andrew Appel

Interaction trees are a general-purpose data structure in Coq for formalizing the behaviors of recursive programs that interact with their environment. ITrees are built of uninterpreted events and their continuations—a coinductive variant of a ``free monad.'' They allow proofs of compositional properties for interpreters built from event handlers and admit a general, mutual recursion operator. ITrees are also executable, e.g. through extraction, making them suitable for debugging, testing, and implementing executable artifacts.

This talk will show how, using this theory, we can prove, in Coq, the termination-sensitive correctness of a compiler from a simple imperative source language to an assembly-like target whose meanings are given as an ITree-based denotational semantics. Crucially, the correctness proof follows entirely by structural induction and the equational theory of combinators for control-flow graphs, which are built on top of the mutual recursion operator.

Sat 22 Jun

Displayed time zone: Tijuana, Baja California change

16:00 - 17:30
Interaction Trees and Algebraic Effects IDeepSpec at 106B
Chair(s): Andrew Appel Princeton
16:00
20m
Talk
Interaction Trees: Representing Recursive and Impure Programs in Coq
DeepSpec
Steve Zdancewic University of Pennsylvania
16:20
25m
Talk
Connecting Separation Logic with First-Order Reasoning on Memory
DeepSpec
William Mansky University of Illinois at Chicago, Wolf Honore
16:45
45m
Talk
Typed Programming with Algebraic Effects (in terms of ambient values, functions, and control)
DeepSpec
Daan Leijen Microsoft Research, USA