The Coq mailing list

[Eduardo Gimenez <Eduardo.Gimenez AT trusted-labs.fr>]

Hello,

I would like to know which is the most appropriate bibliographic reference that 
could uphold the assertion "the type theory underlying the Coq proof environment 
is a strongly normalizing calculus".

By the time I was in the Coq team, there were several proofs, but as far as I 
remember none of them addressed the whole system (some did not address Coq's 
hierarchy of universes, other ones did not address (co)inductive types, and so 
on). In addition to this, I remember that major rearrangements were performed on 
the inclusions between Prop, Set and Type, impredicativity on Set, etc.

Best regards,
Eduardo.