coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Core Verifier of Coq

From: Adam Chlipala <adamc AT csail.mit.edu>
To: coq-club AT inria.fr
Subject: Re: [Coq-Club] Core Verifier of Coq
Date: Sat, 18 May 2013 09:12:58 -0400

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