The Coq mailing list

[Randy Pollack <rpollack AT inf.ed.ac.uk>]

If you want to know how the (pure) Calculus of Conctructions works,
read the Coquand/Huet paper in EUROCAL '85 (LNCS 203) and
Paulin-Mohring's paper in LICS 1986.

There are no inductive types, and definition by impredicative
intersection gives only "weak" iterators; so no constant time
predecessor function.  Also no universes, so it cannot be proven that
booleans true and false are different.  On the other hand some
non-strictly-positive types can be defined impredicatively, although
you can't do much with them.

Randy



On Tue, May 28, 2013 at 12:17 AM, Kenneth Adam Miller
<kennethadammiller AT gmail.com>
 wrote:
> 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?
>