The Coq mailing list

[Robin Adams <radams AT cs.man.ac.uk>]

I am currently working on a formalisation of the metatheory of Pure Type 
Systems in Coq, using a nested data type to represent the terms:

Inductive term : Set -> Type :=
  var : forall V : Set, V -> term V |
  srt : forall V : Set, sort -> term V |
  app : forall V : Set, term V -> term V -> term V |
  pi  : forall V : Set, term V -> term (maybe V) -> term V |
  lda : forall V : Set, term V -> term (maybe V) -> term V.

Thus, term V is the type of all terms that can be formed using the objects
of V as free variables (and the objects of sort as sorts). This idea first
appeared, as far as I am aware, in Bird and Paterson's paper "de Bruijn
Notation as a Nested Datatype" (Journal of Functional Programming 9(1): 
77--91, 1999).

(In fact, to keep everything within Set, I am using a slight variation on 
the above definition.

Inductive term : nat -> Set :=
  var :> forall n : nat, fin n -> term n |
  srt : forall n : nat, sort -> term n |
  app : forall n : nat, term n -> term n -> term n |
  pi : forall n : nat, term n -> term (S n) -> term n |
  lda : forall n : nat, term n -> term (S n) -> term n.)

From what little I've done so far, this approach seems far easier to work 
with than the other two methods of which I am aware: Pollack's "The Theory 
of LEGO", using concrete terms with separate types for the bound variables 
and free variables (parameters); and Barras's project "Coq in Coq", which 
uses the natural numbers as de Bruijn indices.

But I am wary that I might simply be repeating someone else's work.  Does
anyone know of any formalisations of the metatheory of a type theory in
some proof checker following this approach?

--
Robin Adams