Sun 23 Jun 2019 09:45 - 10:30 at 106B - Interaction Trees and Algebraic Effects II Chair(s): Steve Zdancewic

Language designers and implementors in the mechanised era encounter
recurrent problems to do with elementary (eg compilation passes) and
non-elementary (eg logical relations arguments) traversals over object
language expressions which are essentially syntax- (or even type-)

The use of dependent types affords us the opportunity to reify such
operations and proof methods in a manner which is not only scope- and
type-safe at the object level (eg scope-aware pretty-printing, type
preservation ‘for free’) as well as at the meta level (eg not relying
on invocations of possibly-failing tactics), but also generic in both
the structure of traversals, and the structure of syntaxes themselves.

I will illustrate one approach, implemented in Agda, based on a
universe of (descriptions of) binder-aware syntax, with examples
throughout. This is recent joint work with Guillaume Allais, Bob
Atkey, James Chapman and Conor McBride, in particular Guillaume’s
forthcoming PhD thesis.

Sun 23 Jun

Displayed time zone: Tijuana, Baja California change

09:00 - 10:30
Interaction Trees and Algebraic Effects IIDeepSpec at 106B
Chair(s): Steve Zdancewic University of Pennsylvania
Implementation and Verification of Modular Effectful Systems in Coq using FreeSpec
Yann Régis-Gianas IRIF, University Paris Diderot and CNRS, France / INRIA PI.R2
Names, Places, and Things: Generic Traversals over Generic Syntax with Binding
James McKinna University of Edinburgh