The Coq mailing list

[Marco Servetto <marco.servetto AT gmail.com>]

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.