The Coq mailing list

[Jonas Oberhauser <s9joober AT gmail.com>]

Am 05.07.2013 23:03, schrieb t x:
> Hi,
>
>   Is there a formalization of CiC in Coq?
>
>   I recently stumbled across 
> http://www.lix.polytechnique.fr/~barras/coq_work-eng.html 
> <http://www.lix.polytechnique.fr/%7Ebarras/coq_work-eng.html> which 
> appears to only formalize CC in Coq.
>
>   I'm wondering if there is something that defines CiC in Coq. (I feel 
> like reading such definitions in Coq would actually deeper my 
> understanding.)
>
> Thanks!

Hi,

at least not with a proof of termination (i.e., strong normalization). I 
did an extension of Barras' formalization to CC with small sigma types, 
but I'm not aware of any Coq-formalization that covers more of CiC than 
that (when it comes to proving termination) . Anyhow, that's just what I 
recall from the top of my head.

Jonas