The Coq mailing list

["Luo, Zhaohui" <Zhaohui.Luo AT rhul.ac.uk>]

Dear Stefan,

The type theory UTT would be what you are looking for.  Please look at Chapter 9 of the following book:

Z. Luo. Computation and Reasoning: A Type Theory for Computer Science. International Series of Monographs on Computer Science, 11. Oxford University Press, 1994.

The meta-theoretic study of UTT, including a proof of strong normalisation and logical consistency, can be found in Goguen's PhD thesis:

H. Goguen. A Typed Operational Semantics for Type Theory. PhD thesis, University of Edinburgh.1994. LFCS Report ECS-LFCS-94-304.

Best regards,

Zhaohui

---

From: coq-club-request AT inria.fr <coq-club-request AT inria.fr> on behalf of Stefan Monnier <monnier AT IRO.UMontreal.CA>
Sent: 05 November 2018 06:57
To: coq-club AT inria.fr
Subject: Re: [Coq-Club] Proof on strong normalization of cic

 

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.