The Coq mailing list

[Kenneth Adam Miller <kennethadammiller AT gmail.com>]

Jonas: yeah, by now I knew that coq uses the pCiC now, but I suppose what I thought was that in many different references its CoC specifically that's mentioned as the basis; Coq is powerful, so I concluded that it was CoC behind it because that's what the literature mentions. Because I didn't know what the CoC was, there was no way to distinguish between CoC and pCiC or to know that the CoC was so limited.

Cody: ah thanks!

On Thu, May 30, 2013 at 7:46 PM, Cody Roux <cody.roux AT andrew.cmu.edu> wrote:

On 05/30/2013 06:09 PM, Jonas Oberhauser wrote:

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

    To be fair, and I'm aware I'm getting a bit off track here, the CoC already has several features that I consider "incredibly valuable to know and be able to wield", at leas for PL enthusiasts:

- Higher-order functions
- Parametric polymorphism
- Type constructors and higher kinds
- Dependent types

Note that each one of these features corresponds to one facet of the lambda-cube.

Best,

Cody