[FOM] on Bas Spitters on "constructive impredicativity?"

[Gabriel Stolzenberg]

On Thu, 30 Mar 2006, Bas Spitters wrote:

> There is now also an intuitionistic version, i.e. provable in
> Kleene-Vesley's FIM, by Veldman.
>
> (Wim Veldman: An intuitionistic proof of Kruskal's theorem. Arch. Math.
> Log. 43(2): 215-264 (2004))

> This result was elicited by Coquand's result. Veldman's proof is
> predicative and can be translated into a Bishop-style constructive
> proof.

   As I recall, part of the story was that Harvey had proved that
every proof of Kruskal's theorem requires impredicativity.  Obviously,
I must be mistaken about this.  Is there some other result with which
I may be confusing this?
>
> For some time already Coq is based on the calculus of inductive
> constructions (by Coquand and Paulin).

   I'm aware of the pun.  I like Huet's sense of humor.
>
> > Also, how does the shift to predicativity effect type checking?
>
> It is still decidable, if that was your question.
>

   Actually, I was thinking about efficiency.  I had the, possibly
mistaken, impression that the use of impredicativity helped make
for efficient type checking.

   Thanks for the information.

   Gabriel