The Coq mailing list

[Arnaud Spiwack <aspiwack AT lix.polytechnique.fr>]

To be fair, Coq's design has been very strongly influenced by the calculus of construction and in particular the early work of Christine Paulin on impredicative encoding (mentionned by Randy Pollack up-thread). If you are so inclined, reading this paper can bring up a deep understanding of why many things are how they are.

On 31 May 2013 07:12, Kenneth Adam Miller <kennethadammiller AT gmail.com> wrote:

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