coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] A concise formal description of the logic behind Coq

From: Freek Wiedijk <freek AT cs.ru.nl>
To: coq-club AT inria.fr
Subject: Re: [Coq-Club] A concise formal description of the logic behind Coq
Date: Tue, 3 Feb 2015 10:49:17 +0100

Hi David,

>I was hoping that someone could point me at a concise formal description of
>the logic behind Coq. As concise and formal as possible please. Thanks!

That doesn't exist AFAIK.

The best approximation that I know of is appendix A from
<http://arxiv.org/abs/1202.4905>.

Freek

[Coq-Club] A concise formal description of the logic behind Coq, David McAllester, 01/30/2015
- Re: [Coq-Club] A concise formal description of the logic behind Coq, Freek Wiedijk, 02/03/2015
  - Re: [Coq-Club] A concise formal description of the logic behind Coq, Ali Assaf, 02/03/2015