``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 simple case of the setoid model gives a computational interpretation of Church's description axiom. This can be contrasted with a previous attempt which does not provide a convenient notion of definitional equality.
A variation on the setoid model where we get some definitional equality holding in the model. Hopefully this should be enough to interpret weak type theory. This generalizes to get an interpretation in intensional type theory of a weak form of the groupoid model.
The first published version of dependent type theory allows only a weak notion of conversion. The original version uses a system of combinators. We give an alternative formulation. It may be argued, and has been argued by Martin-Lof at some point, that this version represents a better notion of definitional equality.
One main obstacle for interpreting constructively the Kan simplicial set model of type theory is that degeneracy of simplices may not be decidable. This is explained in this paper. It is possible to transform computationally any weak equivalence between two such sets into a path between then (axiom of univalence).
A talk which should give a rather concrete explanation of the model of types as Kan simplicial sets. This gives a model of type theory with equality satisfying the extensionality axiom. However Kan condition is replaced by a more complex property and it is not clear if univalence holds in this model.
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