The Coq mailing list

[Kenneth Adam Miller <kennethadammiller AT gmail.com>]

Thank you all so much! Before we get too distracted, and off topic from the central question, I'd like to iterate over each of the replies and give my thoughts;

Marco, I agree with everything you say. My thirst for knowledge cannot be quenched. I say bring it on.

Thanks for the tip Richard!

Gallais, I'll make a post.

Kristopher - what articles are these? I don't think I know exactly what you're talking about...

Cody, I'll look for them. Thanks!

Randy, maybe this is ignorant, but how could such a "seemingly" restricted system be the foundation of Coq?

On Wed, May 29, 2013 at 11:55 AM, Randy Pollack <rpollack AT inf.ed.ac.uk> wrote:

>> [...]  Also no universes, so it cannot be proven that

>> booleans true and false are different.
> Do you have a reference showing the latter point about universes?

The Independence of Peano's Fourth Axiom from Martin-Löf's Type Theory
without Universes. Journal of Symbolic Logic, 53(3), 1988.

This paper shows (Suc n) ~= n is unprovable without universes, for the
same reason as what I said.  If you make the one (consistent)
assumption that true ~= false (Church booleans), you can the prove
distinctness of all constructors of all Church datatypes.

Randy
--

On Tue, May 28, 2013 at 11:47 PM, Harley D. Eades III
<harley.eades AT gmail.com> wrote:
> Hi, Randy.
>
> On May 28, 2013, at 2:33 PM, Randy Pollack <rpollack AT inf.ed.ac.uk> wrote:
>
>> 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.
> Do you have a reference showing the latter point about universes?
>
> Thanks,
> .\ Harley
>
>>  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?
>>>
>
>