``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)
Talk in Stockholm (December 2011). Towards a constructive version of Kan simplicial sets, limited to the case of dimension < 2.
A revised version of the Bologna talk
A talk given for the 24th AILA meeting, Bologna, February 2011. I try to present V. Voevodsky Univalent Foundation. A new aspect may be a purely axiomatic presentation of equality. (All the proofs have been formally verified in Agda by Nils Anders Danielsson.)
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