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.