[POPLmark] Poplmark Digest, Vol 10, Issue 5

[Dan Licata]

On Jun05, Frank Pfenning wrote:
> There is now a presentation of canonical LF using what we call
> "hereditary substitutions" which are defined as a simple primitive
> recursive functionals (first on the structure of types, then the
> structure of terms).  Decidability of this system is immediate and
> syntactic.  As yet, there is no presentation for only LF itself, but LF
> is a fragment contained in the two papers below if you are curious about
> the technique.

Actually, the draft I mentioned before includes the definition of
hereditary substitution for LF (Figure 5 in Section 2.3), if you don't
want to identify the LF fragment of CLF yourself.

Mechanizing Language Definitions
Robert Harper and Daniel R. Licata
Submitted for publication, April, 2006
http://www.cs.cmu.edu/~drl/pubs/hl06mechanizing/hl06mechanizing.pdf

We simply the state the relevant meta-theoretic results, so you'll have
to consult the sources Frank mentioned for the proofs.

-Dan