Author: Robin Adams
Title: A Formalisation of the Metatheory of Pure Type Systems in Coq
Abstract: 
The idea of representing the syntax of a language with variable binding as
a nested data type --- defining the type "term V" of terms which use the
objects of type V as free variables --- is not new, but seems never to
have been applied to the formalisation of results in the metatheory of a
type theory.  I shall present a formalisation in Coq of several results in
the theory of Pure Type Systems, including the quite difficult proof of
the strengthening lemma, based on this approach to syntax.  I hope to show
that it compares favourably in many ways with previous approaches to the
formalised metatheory of a type theory.