The Coq mailing list

[Jonas Oberhauser <s9joober AT gmail.com>]

Am 30.05.2013 05:26, schrieb Kenneth Adam Miller:
> Randy, maybe this is ignorant, but how could such a "seemingly" 
> restricted system be the foundation of Coq?

Hi Kenneth,

Coq uses the "Predicative Calculus of (Co-)Inductive Constructions" 
(pCiC), which is more powerful than ECC which in turn is far more 
powerful than Martin-Loef's calculus.
I'm under the impression that when you say CoC you mean pCiC; I already 
expected this when you said "My impression is that the Calculus of 
Constructions would be something incredibly valuable to know and be able 
to wield".

Kind regards, Jonas