The Coq mailing list

[Conor T McBride <c.t.mcbride AT durham.ac.uk>]

Hi Robin

Robin Adams wrote:
> 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.
>
> 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).

It's certainly older than that. Bellegarde and Hook look at something of
the sort in `Substitution: A formal methods case study using monads and
transformations.' SCP 23(2-3), 1994.

Independently of Bird and Paterson, Altenkirch and Reus (from whom I got
the above reference) had the same idea as a light snack in `Monadic
presentations of lambda terms using generalized inductive types'
(in Proc. CSL 1999, LNCS 1683); main course is well-scoped *simply-typed*
lambda-terms.

> 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.)
>
> 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?

After reading both B&P and A&R, I developed substitution and its laws for 
untyped lambda-terms in this style using my OLEG system. I'm afraid it's
only written up in my thesis. I used a functional representation of
simultaneous substitution, which did get me into a little
bother with extensionality. More recently, Peter Morris (a student of 
Thorsten's) has developed the same operations in Epigram, but with renamings
and substitutions represented as vectors, hence less bother with
extensionality. I found it a useful technique and am happy to recommend it to
others.

Of course, it takes a lot more than substitution for untyped lambda-terms
to do metatheory of PTSs, so I suspect the application may be novel even if
the representation of terms is not.

Best of luck

Conor