The Coq mailing list

[Cody Roux <cody.roux AT andrew.cmu.edu>]

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