coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] the logic of Coq

From: Gergely Buday <gbuday AT gmail.com>
To: coq-club AT inria.fr
Subject: [Coq-Club] the logic of Coq
Date: Tue, 21 Sep 2010 16:14:55 +0200
Domainkey-signature: a=rsa-sha1; c=nofws; d=gmail.com; s=gamma; h=mime-version:date:message-id:subject:from:to:content-type; b=vWSQL1U5YNt9CY372uy7fiTmyyjDv8X8JnZGU4Bljrqo7QGI3/+kJn+GJlUAepQCdm sP/Bqo1K+SNVSJuBPQ0BnWRpMumWTK8lbRt176pZ3fRSqpcx4P4aYn5KRI8pTEKZPLm6 N3iGi3tXYFmMEOTDMsv07dcDF5S1klsOoswXk=

Hi there,

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 ;?

Or, there were some new developments influencing the kernel code?

- Gergely

[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