Tait in One Big Step

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.