[POPLmark] Poplmark Digest, Vol 10, Issue 5

[Karl Crary]

Please do not put words in my mouth.  I never said that adequacy for Coq 
was implausible; in fact I find it quite plausible.  I simply said that 
it seems that it would have to rely on a (deep) normalization theorem, 
while LF adequacy does not.  Nor was that even intended as a criticism.  
I was merely rebutting the claim that adequacy for LF is somehow 
suspect, whereas adequacy for anything else is trivial.

    -- Karl


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