Type Theory

``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 (2009) about evaluation of open expressions by Per Martin-Lof.

• An old draft (February 1986) paper.

• A variation of Hurkens-Reynolds Paradox.

• Normalisation (2018) for type theory with extension types. The argument may be different from the one using synthetic Tait computability.

• Old note (2009) on forcing in simple type theory inspired by a really nice paper of Levin (1977)

• A paper of Gavin Wraith on impredicative encoding of coinductive definitions

• A short version of my paper on Girard's Paradox (1986)

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

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

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

• Remark on the history of Boolean models

  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)

• Type theory

  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 (written around 2008).

• A calculus of definitions

  Can be the basis of the conversion algorithm in agda

• Completeness theorems and lambda-calculus

  Slides of a TLCA talk in Nara, April 2005

• A Finitary Fragment of System F

  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

• Functional Programming and Type Theory (Göteborg, 95)

• Ordinals in Type Theory (talk given in Aarhus, CSL 97)

• Infinite Objects in Type Theory (to be updated)

• Pattern Matching in Type Theory (to be updated)

• An Algorithm for Type-Checking Dependent Types

  I got several corrections from Bjorn Bringert about the Haskell code. Here is a corrected version

• An Analysis of Girard's Paradox (LICS 1986)

• The paradox of trees in type theory

• Metamathematical Investigations of a Calculus of Constructions (1989) ps version pdf version

• A New Paradox in Type Theory (1991)

• An extract (1989) form the thesis of Paulin-Mohring, with a suggestion of how to add inductive types with an impredicative sort (that was presented in a joint paper)

• A short description of another logical framework (1990)