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.
References
[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.