Discussion:
Proof on strong normalization of cic
(too old to reply)
Helmut Brandl
2018-10-02 23:23:16 UTC
Permalink
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
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
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
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
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
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 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.
Loading...