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-***@inria.fr <coq-club-***@inria.fr> on behalf of Stefan Monnier <***@IRO.UMontreal.CA>

Sent: 05 November 2018 06:57

To: coq-***@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

*Post by Thorsten Altenkirch*#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... :-)

@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

*Post by Stefan Monnier**Post by Helmut Brandl*Unfortunately the text only proves strong normalization for the calculus of

constructions which is the most complex typed lambda calculus of

Barendregts 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.