Papers that may be difficult to find

Talk (2009) about evaluation of open expressions by Per Martin-Lof.

Martin-Lof first paper 1971 on inductive definitions in type theory, still written with Type:Type. This is also the first paper which hints to a connection with computer science.

A paper of Gavin Wraith on impredicative encoding of coinductive definitions

A preliminary version of Harold Simmons' work on ordinal notations (1994)

A internship work of Rosain Johann on computation in HoTT

A quite old (1988) generalised algebraic presentation of type theory due to Thomas Ehrhard, in the Annexe of his PhD thesis. As Thomas noticed, this presentation does not used a pairing operation as primitive.

A paper on universes by Ed Griffor and Erik Palmgren (never published), hinting to a connection with large cardinal axioms (in particular Mahlo cardinal) in set theory.

A paper by Francois Lamarche, which was a motivation for the groupoid model.

Some slides of a talk of David Turner (May 1989) on extensional type theory.

A short paper on Dummett by Gabriel Stolzenberg.

An old draft (February 1986) paper.

A paper of Louise Leclerc on Eilenberg-MacLane spaces

Decidability of conversion for type theory
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.

Last modified: Fri Sep 13 22:08:32 MET DST 2002