The Coq mailing list

[Jonas Oberhauser <s9joober AT gmail.com>]

Am 31.05.2013 01:46, schrieb Cody Roux:
> 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 

Getting even further off track,

I agree that it's a very interesting system to study, but I wouldn't say 
that it's "INCREDIBLY valuable to be able to wield" (which I would say 
for pCiC).
Note that kinds in CoC have a very restricted form (e.g., no variables 
or applications), and it should be easy to see how this restriction 
limits the calculus.
On the other hand, this restriction makes a couple of really nice 
termination proofs (in the spirit of Geuver's 'short and flexible' 
proof) go through, which do not (easily?) extend to stronger systems 
where this restriction is less severe (e.g., ECC or even just CoC with 
one additional universe).

Kind regards,
Jonas