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

09:00 - 10:30: DeepSpec 2019 - Interaction Trees and Algebraic Effects II at 106B
Chair(s): Steve ZdancewicUniversity of Pennsylvania
deepspec-2019-papers09:00 - 09:45
Yann Régis-GianasIRIF, University Paris Diderot and CNRS, France / INRIA PI.R2
deepspec-2019-papers09:45 - 10:30
James McKinnaUniversity of Edinburgh