We present a Tait-style proof to show that a simple functional normaliser for a combinatory version of System T terminates. Using a technique pioneered by Bove and Capretta, we can implement the normaliser in total Type Theory. The main interest in our construction is methodological, it is an alternative to the usual small-step operational semantics on the one side and normalisation by evaluation on the other. The present work is motivated by our longer term goal to verify implementations of Type Theory such as Epigram.
Author and article information
School of Computer Science and IT, University of Nottingham
Jubilee Campus, Wollaton Road, Nottingham NG8 1BB, UK