The Coq mailing list

[Frédéric Blanqui <frederic.blanqui AT inria.fr>]

Hello.

Note that CoC is already rich enough to represent any function whose 
termination is provable in higher-order arithmetic...

Frédéric.

Le 31/05/2013 18:39, Jonas Oberhauser a écrit :
> 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