The Coq mailing list

[Bas Spitters <b.a.w.spitters AT gmail.com>]

Thanks (I should have mentioned Bruno's work).

It would be good to record these works and their limitations.
I did not find an entry in cocorico, for instance.

On Fri, Jul 7, 2017 at 9:02 AM, Amin Timany 
<amintimany AT gmail.com>
 wrote:
> Hi Bas,
>
> It is indeed one of them. This paper establishes consistency by constructing
> a set theoretic model and showing the interpretation of the type false is
> indeed empty. Another one is  Bruno Barras’ habilitation
> http://www.lix.polytechnique.fr/~barras/habilitation/. He proves strong
> normalization for CIC and all proofs are also formalized Coq itself on top
> of an axiomatization of IZF (Intuitionistic ZF).
>
> It should be noted though that these are not formalizing exactly what we in
> Coq but they are pretty close. For example, if I’m not mistaken, neither of
> them considers inductive types in Prop or eta expansion.
>
> Regards,
> Amin
>
> On 7 Jul 2017, at 09:07, Bas Spitters 
> <b.a.w.spitters AT gmail.com>
>  wrote:
>
> https://coq.inria.fr/faq
> "Proofs of consistency of *subsystems* of the theory of Coq can be
> found in the literature."
>
> Is this what is intended?
> Proof-irrelevant model of CC with predicative induction and judgmental
> equality
> Lee-Werner
> https://arxiv.org/abs/1111.0123
>
> It might be good to add some references to the FAQ.
>
>