The Coq mailing list

[Chris Casinghino <chris.casinghino AT gmail.com>]

Hi all,

I'm curious about how much of the metatheory of Coq (or similar type
theories) has been formalized in Coq itself.  I'm particularly
interested in proofs of strong normalization/logical consistency.  I
know that Barras and Werner mechanized strong normalization of CC in
the "Coq in Coq" paper.  Has anyone done more?  In particular, has
anyone added data types, recursion, large eliminations, or a universe
hierarchy to these proofs?  Is there any speculation about how far one
could get before running up against Godel?

I've been looking at Bruno Barras' thesis, which seems to formalize
some of the metatheory of coq.  But, I don't speak any French so I'm
having trouble determining whether it does normalization or just type
safety.  And I haven't been able to track down the corresponding coq
scripts.

Thanks for your help!

--Chris Casinghino