[POPLmark] Poplmark Digest, Vol 10, Issue 5

[Aaron Stump]

> There is no contest.  The proof theoretic strength alone that is
> required to carry out the normalization proof for Coq is much, much
> higher than LF.  It took the genius of Girard to develop the method of
> "candidats" to give the first normalization proof for the polymorphic
> lambda-calculus; normalization for LF is of the same complexity as the
> simply typed lambda calculus (extensionality or not).

The proof theoretic strength is definitely relevant, but my point still
remains.  The meta-theories of both LF and Coq required very serious
work by top researchers over substantial numbers of years to develop.
The definitive accounts of LF's meta-theory, both the old approach and
the new one you mentioned, are only rather recently published (2005 and
2004, if I am not mistaken).  Thus, I believe it is misleading to
suggest, as Karl seemed to be doing, that adequacy for LF is a totally
trivial result, while for something like Coq it is so deep as to be
implausible.  

The relative proof theoretic weakness of LF may indeed give it an
advantage for many applications.  As you note, however, for development
of constructive mathematics as in POPLmark, a richer theory may be
desirable.

Aaron