[Coq-Club] Proof on strong normalization of cic

Discussion:

Helmut Brandl

2018-10-02 23:23:16 UTC

Hi coq-list,

can anybody give me a link to a proof of strong normalization of the calculus of inductive constructions used in coq.

It is easy to find proofs for many kinds of typed calculi e.g. simply typed lambda calculus, … even pure type systems and calculus of constructions. But I have not found a proof for cic.

Thanks for any hint.
Regards
Helmut

William J. Bowman

2018-10-02 23:34:07 UTC

Permalink

I understand that Bruno Barras' habilitation
(http://www.lix.polytechnique.fr/~barras/habilitation/) shows strong
normalization for CIC.
I found this from a prior thread on this mailing list:
https://sympa.inria.fr/sympa/arc/coq-club/2017-07/msg00015.html

--
William J. Bowman

Post by Helmut Brandl
Hi coq-list,
can anybody give me a link to a proof of strong normalization of the calculus of inductive constructions used in coq.
It is easy to find proofs for many kinds of typed calculi e.g. simply typed lambda calculus, … even pure type systems and calculus of constructions. But I have not found a proof for cic.
Thanks for any hint.
Regards
Helmut

Helmut Brandl

2018-10-03 03:38:12 UTC

Permalink

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.

Helmut

Post by William J. Bowman
I understand that Bruno Barras' habilitation
(http://www.lix.polytechnique.fr/~barras/habilitation/) shows strong
normalization for CIC.
https://sympa.inria.fr/sympa/arc/coq-club/2017-07/msg00015.html
--
William J. Bowman

Bas Spitters

2018-10-03 05:31:12 UTC

Permalink

A bit of discussion is here:
https://github.com/coq/coq/wiki/CoqTerminationDiscussion

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

Stefan Monnier

2018-10-03 11:59:00 UTC

Permalink

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

Thorsten Altenkirch

2018-10-04 06:38:48 UTC

Permalink

#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

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
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 Nottingh

Stefan Monnier

2018-11-05 06:57:31 UTC

Permalink

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

Luo, Zhaohui

2018-11-05 08:17:49 UTC

Permalink

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