Pure Type Systems in Coq

I am currently working on a formalization of the metatheory of Pure Type Systems (PTSs) in Coq, based on the representation of terms as a nested datatype [2, 5, 7].  You can have a look at the source code and the documentation automatically produced by coqdoc here, as well as the current state of my own documentation, which is proceeding slowly.

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.
[1]   Robin Adams, 2005.  Pure Type Systems with Judgemental Equality.  To appear in J. Functional Programming.
[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.