coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] the logic of Coq

From: Adam Chlipala <adam AT chlipala.net>
To: Gergely Buday <gbuday AT gmail.com>
Cc: coq-club AT inria.fr
Subject: Re: [Coq-Club] the logic of Coq
Date: Tue, 21 Sep 2010 10:33:40 -0400

Gergely Buday wrote:

do I understand correctly that the underlying logic of Coq is the
extended calculus of constructions, as described in

http://www.cs.rhul.ac.uk/~zhaohui/THESIS90.ps ;?

No, Coq is based on the Calculus of Inductive Constructions, which is described to some extent in Chapter 4 of the Coq manual (though people often complain that there isn't a clear presentation [in English] of the precise theory behind Coq).

[Coq-Club] the logic of Coq, Gergely Buday
- Re: [Coq-Club] the logic of Coq, Adam Chlipala
- <Possible follow-ups>
- Re: [Coq-Club] the logic of Coq, Cody Roux