The Coq mailing list

[Frédéric Blanqui <frederic.blanqui AT inria.fr>]

Hello.

I would like to mention also http://dl.acm.org/citation.cfm?id=1227232:

The open calculus of constructions (part I): an equational type theory 
with dependent types for programming, specification, and interactive 
theorem proving,

Mark-Oliver Stehr,

Fundamenta Informaticae 68(1-2):131-174, 2005.


Le 07/07/2017 à 15:25, Bas Spitters a écrit :
> Lee-Werner seem to lack coinductive types, modules, but also have:
> Prop:Type0
> However, Coq has:
> Prop:Type1
> https://coq.inria.fr/refman/Reference-Manual006.html
>
> Lee-Werner observe that:
> In this paper, we do not consider the sort Set. Indeed, when (the
> impredicative or predicative sort)
> Set is placed at the lowest level in the hierarchy of sorts, as in the
> case of the current development of Coq, there is no way to provide a
> universal set-theoretic interpretation of both Set and Prop, as
> identified by [Reynolds(1984)].
>
> On Fri, Jul 7, 2017 at 9:07 AM, Bas Spitters 
> <b.a.w.spitters AT gmail.com>
>  wrote:
> > 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.