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