I began this work because I wanted a machine-checked version of my result on the equivalence of systems with and without equality judgements [1]. I looked at two previous formalizations of the metatheory of type theories [4, 8]; neither was satisfactory for my purposes, so I set about building my own from scratch. I think the results are quite satisfactory.

This formalisation follows the development in [3] faithfully, proceeding then to the proof of the Strengthening Lemma in [6]. I have also formalized the results in Appendix B of [1], and have begun on the results in the main body of the paper.

The documentation is now thoroughly out of date, and I am sure the file Strength.v could be simplified further, but I would like for the moment to press ahead and complete the formalization of the main result in [1].

Finite.v - Some preliminaries dealing with a family of finite types.

Terms.v - The definition of the family of types of terms.

Subvar.v - The operation of replacing variables.

Subst.v - The operation of substitution.

Conv.v - Beta-reduction and beta-conversion.

CR.v - The Church-Rosser Theorem.

PTS.v - The rules of deduction of a Pure Type System.

Meta.v - The basic metatheory, including Weakening, Substitution and Generation Lemmas.

SR.v - The Subject Reduction Theorem.

UT.v - Uniqueness of types in a functional PTS

String.v - Results about strings of terms needed for:

Strength.v - Van Bentham Jutting's proof of the Strengthening Lemma [6].

PTSeq.v - Basic metatheory of Pure Type Systems with judgemental equality.

Labterms.v - The definition of the family of types of labelled terms used by TPOSR.

Labsubvar.v - The operation of replacing variables in labelled terms.

Labsubst.v - The operation of substitution on labelled terms.

Labconv.v - Beta-reduction and beta-conversion on labelled terms.

Labctxt.v - Labelled contexts.

TPOSR.v - Typed Parallel One-Step Reduction.

Documentation - Here is how much of the project I have managed to document so far. Quite out of date, I am afraid.

[2] Thorsten Altenkirch and Bernhard Reus, 1999. Monadic Presentations of Lambda Terms using Generalized Inductive Types. CSL '99, LNCS 1683, 453-468. Springer-Verlag.

[3] Hank Barendregt, 1992. Lambda Calculi with Types. In Abramsky, Gabbat and Maibaum (eds.) Handbook of Logic in Computer Science, Vol. II. Oxford University Press.

[4] Bruno Barras, 1999. Auto-validation d'un système de preuves avec familles inductives. PhD thesis, Université Paris 7.

[5] Francoise Bellegarde and James Hook, 1994. Substitution: A formal methods case study using monads and transformations. Science of Computer Programming 23 (2-3), 287-311.

[6] L. S. van Bentham Jutting, 1993. Typing in Pure Type Systems. Information and Computation 105 (1), 35-41.

[7] Richard S. Bird and Ross Patterson, 1999. De Bruijn Notation as a Nested Datatype. J. Functional Programming 9 (1), 77-91.

[8] James McKinna and Robert Pollack, 1999. Some Lambda Calculus and Type Theory Formalized. Journal of Automated Reasoning 23 (3-4), 373-409.

Here is the documentation produced by coqdoc: coqdoc documentation.

Last updated 28/4/06.