The Coq mailing list

[Richard Dapoigny <richard.dapoigny AT univ-savoie.fr>]

Le 28/05/2013 06:17, Kenneth Adam Miller a écrit :
> My impression is that the Calculus of Constructions would be something
> incredibly valuable to know and be able to wield. Since it was born within the
> past few decades, I had surmised that it hadn't hit mainstream because the
> learning curve is incredibly high and because its so new; are these correct?
>
> Also, when reading the Coq'Art book, I find that there are a number of subtle
> and even explicit references to the CoC, and I want to be able to understand
> the CoC fundamentally in order to draw the most out of this book. I searched
> everywhere for the original publication that was cited in the book, but
> couldn't find it available on the open web. Would anybody know where a good
> set of materials might be, other than the Software Foundations or Coq'Art
> book, both of which I already have access to?
Hi,
To my knowledge there are no books about the CoC strictly speaking, 
however you can read "Computation and reasoning" written by Zaohui Luo. 
This is about ECC, the Extented Calculus of Constructions in which you 
will find many details clearly stated. Major differences with the CoC 
(with universes) are the subtyping (cumulativity) which is processed 
with coercions in Coq and the neta-rule not available in ECC. However 
there are many explanations that may interest you.
Cheers
Richard

--
And the wounded skies above say
it's much too much too late.
Well, maybe we should all be praying for time.

begin:vcard
fn:Richard Dapoigny
n:Dapoigny;Richard
email;internet:richard.dapoigny AT univ-savoie.fr
tel;work:+33 450 09 65 29
tel;cell:+33 621 35 31 43
version:2.1
end:vcard