The Coq mailing list

[Math Prover <mathprover AT yahoo.com>]

Hi Jonas,

This was actually next on my reading list. Would have read it earlier had I realized it had what I needed. :-)

---

From: Jonas Oberhauser <s9joober AT gmail.com>
To: coq-club AT inria.fr; Math Prover <mathprover AT yahoo.com>
Sent: Saturday, May 18, 2013 2:48 AM
Subject: Re: [Coq-Club] Core Verifier of Coq

Am 18.05.2013 03:29, schrieb Math Prover:

Hi Coq-Club,

  With apologies for my ignorance, can someone point me at the documentation for the core verifier of Coq?

  I've played with Coq for a few months now -- working through parts of Pierce's Software Foundations and Chlipala's CPDT, however despite proving some non-trivial theorems, I often feel that I don't understand "what's going on under the hood."

  What I'm looking for is the equivalent of

  * SICP's meta circular evaluator or

  * the epsilon-delta definition of derivatives

  If we view a 'state' as

  pair<list<hypothesis>, goal>

  Then there should be a minimal set of rules for deriving new 'states.'

  I'm looking for the minimal set of rules on top of which all valid proofs are built.

Thanks!

Hi Math prover,

You should check the book Coq'Art, which I recall gives a very nice explanation of the theoretical framework of Coq.

Kind regards, Jonas