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-)
directed.

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.