``Every constructive proof can be regarded as the development of a (possibly) new notation, and the verification that certain computations performed with the aid of that notation produce certain results.'' (Bishop)
A quite direct proof, based on a model construction. In 91, I had the following proof If we adopt the remarks in this note we get an argument that has recently been checked in Agda.
Boolean models in type theory, as presented by Church, using an idea of Lagerstrom. Interestingly, what is missing is a treatment of propositional extensionality (two equivalent propositions are equal)
A talk given for Bengt's 60th birthday (2009). The goal was to have a complete presentation of an implementation type theory, as simple as the first version of LISP. It would be nice if this can be extened to extensional equality. Here is a corresponding description of one way to implement type theory (written around 2008).
Can be the basis of the conversion algorithm in agda
Slides of a TLCA talk in Nara, April 2005
We give a fragment of system F which has a finitary normalisation proof
Here is a simplification of the previous proof, using comments from Buchholz A Finitary Fragment of System F
Slides Overhead presenting this result
I got several corrections from Bjorn Bringert about the Haskell code. Here is a corrected version