The Coq mailing list

[Ali Assaf <ali.assaf AT inria.fr>]

Hello,

You can also take a look at the Coq manual, chapters 4 and 5:
https://coq.inria.fr/refman/Reference-Manual006.html
https://coq.inria.fr/refman/Reference-Manual007.html

Bear in mind that the actual implementation deviates on some points, so that 
in the end the only 100% precise and correct specification is the code itself.

Best,

Ali Assaf

----- Original Message -----
> From: "Freek Wiedijk" 
> <freek AT cs.ru.nl>
> To: 
> coq-club AT inria.fr
> Sent: Tuesday, February 3, 2015 10:49:17 AM
> Subject: Re: [Coq-Club] A concise formal description of the logic behind Coq
> 
> 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
>