This repository contains a proof that the simply typed lambda calculus is strongly normalizing im Agda. The proof uses an approach using a logical predicate. This version is mostly based on work by Altenkirch et al. We use an intrinsically-typed de Bruijn representation originally due to Altenkirch and Reus. A rendered version of the files can be found here.
- Thorsten Altenkirch, Bernhard Reus, Monadic Presentations of Lambda Terms Using Generalized Inductive Types. CSL 1999
- Thorsten Altenkirch, A Formalization of the Strong Normalization Proof for System F in LEGO. TLCA 1993
- Thorsten Altenkirch, Constructions, inductive types and strong normalization. University of Edinburgh, UK
- Agda, Version 2.6.2.2
- Agda Standard Library