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
Times are displayed in time zone: (GMT-07:00) Tijuana, Baja California change

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