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 . 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  faithfully,
proceeding then to the proof of the Strengthening Lemma in . I
have also formalized the results in Appendix B of , 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 .
Finite.v - Some preliminaries dealing with a
family of finite types.
Terms.v - The definition of the family of types
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
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
Strength.v - Van Bentham Jutting's proof of
the Strengthening Lemma .
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.
 Robin Adams, 2005. Pure Type Systems with Judgemental Equality.
To appear in J. Functional Programming.
 Thorsten Altenkirch and Bernhard Reus, 1999. Monadic Presentations of Lambda Terms
using Generalized Inductive Types. CSL '99, LNCS 1683,
 Hank Barendregt, 1992. Lambda Calculi with Types. In
Abramsky, Gabbat and Maibaum (eds.) Handbook
of Logic in Computer Science, Vol. II. Oxford University
 Bruno Barras, 1999. Auto-validation d'un système de
preuves avec familles inductives. PhD thesis,
Université Paris 7.
 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.
 L. S. van Bentham Jutting, 1993. Typing in Pure Type Systems.
Information and Computation 105 (1), 35-41.
 Richard S. Bird and Ross Patterson, 1999. De Bruijn Notation as a Nested Datatype.
J. Functional Programming 9 (1), 77-91.
 James McKinna and Robert Pollack, 1999. Some Lambda Calculus and Type Theory
Formalized. Journal of Automated Reasoning 23 (3-4),
Here is the documentation produced by coqdoc: coqdoc documentation.
Last updated 28/4/06.