coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Proof on strong normalization of cic

From: Helmut Brandl <helmut.brandl AT gmx.net>
To: coq-club AT inria.fr
Subject: Re: [Coq-Club] Proof on strong normalization of cic
Date: Tue, 2 Oct 2018 22:38:12 -0500
Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=helmut.brandl AT gmx.net; spf=Pass smtp.mailfrom=helmut.brandl AT gmx.net; spf=None smtp.helo=postmaster AT mout.gmx.net
Ironport-phdr: 9a23:S2r8NRXK8xXbtZN6+U92VvXp1pTV8LGtZVwlr6E/grcLSJyIuqrYYxOAt8tkgFKBZ4jH8fUM07OQ7/i/HzRYqb+681k6OKRWUBEEjchE1ycBO+WiTXPBEfjxciYhF95DXlI2t1uyMExSBdqsLwaK+i764jEdAAjwOhRoLerpBIHSk9631+ev8JHPfglEnjWwba9wIRmssQndqtQdjJd/JKo21hbHuGZDdf5MxWNvK1KTnhL86dm18ZV+7SleuO8v+tBZX6nicKs2UbJXDDI9M2Ao/8LrrgXMTRGO5nQHTGoblAdDDhXf4xH7WpfxtTb6tvZ41SKHM8D6Uaw4VDK/5KptVRTmijoINyQh/W7LhcN+kaJVrxCvqRJwwIDUbp+bOv1lc6PBZNMaQHZNXsZNWyFDBI63cosBD/AGPeZdt4TzpUUBrR+7BQmxGOPk1yJFhmXs0q08zushFRzN0QsgH90QtHTUqcj1NLsIXe+u1qnH1zPDYO5S2Trm54jIdx8greuKXb1ubcrc0E8iHB7LgFWXrIzqJTKV1uIVvmia6epgT+OvhHQ9pwF/uDij3t8sio7NhoMV1lDL6zl2wIYzJd25UU57fMCrHIFetyGAMYZ9X8AsQ3lwtSok17EKp4S3cDYUxJkl3RLTdvyKf5KV7h/gTOqdPyt0iG9/dL+7hRu+61WsxvH/W8Wu0VtHqDdOnMPWuXAXzRPT79CKSvtj8Uel3jaCzwXT6uZZIUAoj6bbJJshw7EqmpoVr0vDAjf6mETwjKCIakUp4vak5/n5brn8uJOQKY15hhvjPqkugMCzHOc1PhALX2eB+OS80LPj/Vf+QLVPlvA2krfWsJTfJcQGuq61GRRa0pw55Ba5Ejim1M8VnXYCLFNKYh6HiZbmO03WLPDiEfi/m0iskCtsx/3eIrLhBYzNImHfn7flYLZy8FVRyBEzzNBa/5JbEKsNIPP1Wk/rtdzXFAU1MwKuw7WvNNIo3YQHHGmLH6WxMaXIsFbO6Ph8DfOLYdo1tTL4NuRtzeTni3M90QsdcK2swIdRYmqxGPhiC0qccTzqj8tXQjRChRY3UOG/0A7KajVUfXvnB/tttAF+M5qvCML4fq7ohbWA2CmhGZgHNG9DGhaKHGu6LtzYCcdJUzqbJ4paqhJBTaKoGt0u0AHosgLmmeI+c7jkvxYAvJem7+Bbou3ekRZrqW5xCNmBlW6IXydyk39aHzI=

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

> On Oct 2, 2018, at 18:34, William J. Bowman
> <wjb AT williamjbowman.com>
> wrote:
>
> 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
>
> On Tue, Oct 02, 2018 at 06:23:16PM -0500, Helmut Brandl wrote:
>> 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

[Coq-Club] Proof on strong normalization of cic, Helmut Brandl, 10/03/2018
- Re: [Coq-Club] Proof on strong normalization of cic, William J. Bowman, 10/03/2018
  - Re: [Coq-Club] Proof on strong normalization of cic, Helmut Brandl, 10/03/2018
    - Re: [Coq-Club] Proof on strong normalization of cic, Bas Spitters, 10/03/2018
    - Re: [Coq-Club] Proof on strong normalization of cic, Stefan Monnier, 10/03/2018
      - Re: [Coq-Club] Proof on strong normalization of cic, Thorsten Altenkirch, 10/04/2018