The Coq mailing list

[Kristopher Micinski <krismicinski AT gmail.com>]

I would recommend that you read the Coq'Art book for getting a very
pragmatic description of Coq's internals.

As technical as it is, however, the Coq manual is (in my mind, at
least) quite comprehensible!  The core is a proof checker (what
happens after you type "Qed") surrounded by a proof development
environment.  Were you looking for the source to the kernel itself
(unimaginatively named `kernel/` in Coq's source tree)?

For learning the logic at a technical level as it applies to Coq, I'd
recommend reading Coq'Art and then the manual, possibly supplemented
by the papers referenced in the manual (since it doesn't have quite a
comprehensive explanation on things like e.g., coinduction).

Kris


On Sat, May 18, 2013 at 9:27 AM, Math Prover 
<mathprover AT yahoo.com>
 wrote:
> Professor Chlipala, you're right.
>
> Chapter 4: http://coq.inria.fr/refman/Reference-Manual006.html#sec171
>
> (I started out with reading the Coq manual, found it incomprehensible, 
> moved to other tutorials, and unfortunately haven't taken a 2nd look at the 
> manual in detail.)
>
> ________________________________
> From: Adam Chlipala 
> <adamc AT csail.mit.edu>
> To: 
> coq-club AT inria.fr
> Sent: Saturday, May 18, 2013 6:12 AM
> Subject: Re: [Coq-Club] Core Verifier of Coq
>
>
>
>
> On 05/18/2013 05:48 AM, Jonas Oberhauser wrote:
> Am 18.05.2013 03:29, schrieb Math Prover:
>>
>>
>>>
>>>
> With apologies for my ignorance, can someone point me at the
> documentation for the core verifier of Coq?
>>Hi Math prover,
>>
>>You should check the book Coq'Art, which I recall gives a very nice
> explanation of the theoretical framework of Coq.
>>
> There's also a chapter of the Coq manual, right?