``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.
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.
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