The Coq mailing list

[Kristopher Micinski <krismicinski AT gmail.com>]

I also think this would be valuable, given that there are bits of Coq that I only understand at a hand wavy level.

I will say that Coquand's articles are actually pretty readable, you might try those.  However, they don't qualify as a comprehensive treatments with notes and explanations (for someone who doesn't have background).

The manual is also quite good, in terms of its view of CoC.  Coq implements pCiC now, and certain parts of the logic appear piecemeal throughout papers (e.g., coinduction, etc..) instead of as a whole.

Kris

On Tue, May 28, 2013 at 12:48 AM, Marco Servetto <marco.servetto AT gmail.com> wrote:

Indeed, I think is is a good time for that some really expert in coq
and Calculus of Constructions to write a self contained scientific
article explaining to type theory guys
-the theoretical basis of Calculus of Constructions with small step
reduction and "type system"
-using some example show how layers of syntactic sugar over the
primitive Calculus of Constructions can turn it in the usable language
coq.
-(minor need) explaining how that can be connected with the concept of
truth, indeed that is a point I have always missed...

I expect many articles that show progresses over Coq to be out there,
but, I suspect there is no -recent- summary on the whole thing.
I would be incredibly happy to read a work like that, but I can not
afford to invest time to read Coq'Art.