coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Core Verifier of Coq

From: Math Prover <mathprover AT yahoo.com>
To: Adam Chlipala <adamc AT csail.mit.edu>, "coq-club AT inria.fr" <coq-club AT inria.fr>
Subject: Re: [Coq-Club] Core Verifier of Coq
Date: Sat, 18 May 2013 06:27:02 -0700 (PDT)
Domainkey-signature: a=rsa-sha1; q=dns; c=nofws; s=s1024; d=yahoo.com; h=X-YMail-OSG:Received:X-Rocket-MIMEInfo:X-Mailer:References:Message-ID:Date:From:Reply-To:Subject:To:In-Reply-To:MIME-Version:Content-Type:Content-Transfer-Encoding; b=RKPpJwSI2wFRnoV1MNhcMfoLd/UuCzdvApekzkRCNYibItI5m7MNbV/ziuqpa3sTVfUCekT36JeN/9BB17gF8aYrFEKTuZXFUKoBfqkDnqIfvidXObRSfAtuHMi4nCW4vTPuAtCpgDaLQOg7R+CGUBi9kvN7wxNLA5rtjnR8kFI=;

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?

[Coq-Club] Core Verifier of Coq, Math Prover, 05/18/2013
- Re: [Coq-Club] Core Verifier of Coq, Jonas Oberhauser, 05/18/2013
  - Re: [Coq-Club] Core Verifier of Coq, Math Prover, 05/18/2013
  - Re: [Coq-Club] Core Verifier of Coq, Adam Chlipala, 05/18/2013
    - Re: [Coq-Club] Core Verifier of Coq, Math Prover, 05/18/2013
      - Re: [Coq-Club] Core Verifier of Coq, Kristopher Micinski, 05/23/2013