The Coq mailing list

[Cody Roux <cody.roux AT andrew.cmu.edu>]

Hello,

    I find that the article by Simon Peyton Jones and Erik Meijer:

    "Henk: a typed intermediate language"

Does a nice job of exposing the a type system very similar to the CoC in 
a way that programing language enthusiasts might find more familiar, and 
it is quite short.

There is also J.-W. Roorda's master's thesis on the same subject:

    "Pure Type Systems for Functional Programming"

But it is a bit more technical and longer, so it might be harder to 
invest time on it :)

The first chapter of Ulf Norell's PhD dissertation can serve as well, 
though it presents a system different than the CiC in some (small) details.

Best,

Cody


On 05/28/2013 12:48 AM, Marco Servetto 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.