Speaker: Joey Capper
Title: Complete Normalisation in Type Theory
Abstract:
A general technique for showing the completeness of normalisation is presented in the context of Godel's System T.
The technique, first described by Nils Anders Danielsson for a dependently-typed calculus [1], operates by indexing the codomain of the normalisation procedure on its domain.
The additional index allows one to track the relationship between the input and output of the normalisation function.
A simple preservation proof from the indexed to non-indexed variants of the codomain is then all that is required to derive the final completeness theorem.
[1] A Formalisation of a Dependently Typed Language as an Inductive-Recursive Family. Nils Anders Danielsson. Types for Proofs and Programs, International Workshop, TYPES 2006, Revised Selected Papers, LNCS 4502, 2007.