The Coq mailing list

[Stefan Monnier <monnier AT IRO.UMontreal.CA>]

BTW, I've just gone back to those various papers and can't seem to find
one that proves consistency of a lambda calculus that combines:

- impredicativity in the bottom universe (Prop/Set)
- a tower of universes
- inductive types

More specifically, I'm interested in proofs for calculus with inductive
types that can live not only in Prop/Set but also in other universes (as is
the case in Coq, obviously).


        Stefan


Thorsten Altenkirch 
<Thorsten.Altenkirch AT nottingham.ac.uk>
 writes:

> #MeToo
>
> @PhdThesis{alti:phd93,
>   author =     "Thorsten Altenkirch",
>   title =      "Constructions, Inductive Types and Strong Normalization",
>   school =     "University of Edinburgh",
>   year =       "1993",
>   month =      "November",
> }
>
> http://www.cs.nott.ac.uk/~psztxa/publ/phd93.pdf
>
> Ok, I didn't do it in general for inductive types but just for an example.
> The rest I planned to do in a journal paper, still forthcoming... :-)
>
> But the basic idea is explained here:
>
> @InProceedings{alti:types94,
>   author =     "Thorsten Altenkirch",
>   title =      "Proving Strong Normalization of {CC} by Modifying
>                 Realizability Semantics",
>   editor =     "Henk Barendregt and Tobias Nipkow",
>   series =     "LNCS 806",
>   pages =      "3 - 18",
>   booktitle =  "Types for Proofs and Programs",
>   year =       "1994",
> }
>
> http://www.cs.nott.ac.uk/~psztxa/publ/types94.pdf
>
>
> On 03/10/2018, 12:59, 
> "coq-club-request AT inria.fr
>  on behalf of Stefan
> Monnier" 
> <coq-club-request AT inria.fr
>  on behalf of 
> monnier AT IRO.UMontreal.CA>
> wrote:
>
>>> Unfortunately the text only proves strong normalization for the
>>>calculus of
>>> constructions which is the most complex typed lambda calculus of
>>> Barendregt’s lambda cube. As far as I understand no proof of strong
>>> normalization of the calculus of inductive constructions as used in coq
>>>is
>>> contained. However thanks for the link.
>>
>>Benjamin Werner's thesis "Une Théorie des Constructions Inductives" has
>>a proof for the CIC (but without the tower of universes).
>>
>>
>>        Stefan
>
>
>
>
> This message and any attachment are intended solely for the addressee
> and may contain confidential information. If you have received this
> message in error, please contact the sender and delete the email and
> attachment. 
>
> Any views or opinions expressed by the author of this email do not
> necessarily reflect the views of the University of Nottingham. Email
> communications with the University of Nottingham may be monitored 
> where permitted by law.