coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] Proof on strong normalization of cic

From: Helmut Brandl <helmut.brandl AT gmx.net>
To: coq-club AT inria.fr
Subject: [Coq-Club] Proof on strong normalization of cic
Date: Tue, 2 Oct 2018 18:23:16 -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:ZrLu9RZDA0SpZwhdIuwC917/LSx+4OfEezUN459isYplN5qZoMy/bnLW6fgltlLVR4KTs6sC17KJ9fi4EUU7or+5+EgYd5JNUxJXwe43pCcHRPC/NEvgMfTxZDY7FskRHHVs/nW8LFQHUJ2mPw6arXK99yMdFQviPgRpOOv1BpTSj8Oq3Oyu5pHfeQpFiCa/bL9oMBm6sRjau9ULj4dlNqs/0AbCrGFSe+RRy2NoJFaTkAj568yt4pNt8Dletuw4+cJYXqr0Y6o3TbpDDDQ7KG81/9HktQPCTQSU+HQRVHgdnwdSDAjE6BH6WYrxsjf/u+Fg1iSWIdH6QLYpUjmk8qxlSgLniD0fOjA57G7ZhcN/gqxGrhyiuRJxxJXZYJ2MNPp7Yq/dfc8WSGhHU81MVyJBGIS8b44XAuQDI+lYq4z9p0YSrRCjGASsHvngyjlViX/ywKY31OQhHh/C3AwlAtIOrG7Yo87vNKgIV+C60a3IwC7Mb/NT1jbx8o7IfQ49ofyVW797bMnfyVE3Gg/bk1mct5bpMy2L2ukPqWSX8uhtWfixh2I6sw19vCSjyto2hoTNhI8Z0E3I+Tl6zYovJNC1TlNwb8S+H5tKrS6aMpN7QsM8TGFsvyY30rgGuZmmfCgW0pgnyBvfavOdf4iO/B3jSP6dITZ+hH17ZLKynwi+/VW+xuHmSMW4zlRHojBYntTOrHwByQHf5tCCSvRn/0eh3TiP1xrU6uFBOU00lbTUK5okwr4tipofq1/MHjXsl0XwkaCWcl4p+uet6+XoeLnmoIGTN5NshgHkLqsugtC/Afg/MgUWQ2eb/v282KT/8k39XbVFleY7krLZsZDfPcQUvLS1Aw5T0oY56hawFS2q0NoCnSpPEFUQcxWeyoPtJlvmIfbiDP75jU7/vi1swqXmM7nkH4mFBGLKlrvlNeJ95kpZ1RZ1x8pW4Z5QIr4EMLT1V1On54+QNQMwLwHhm7WvM956zI5LATveUJ/cC7vbtBqz3sxqJuCNYIEPvzOsefcg97jogGNrwAZBL5ns5oMebTWDJtojO1+QMCjjh8dHF2oW7FJnEb7azWaaWDsWXE6cGqIx4jZiVNCjCprfAI+okPqH0TvpRpA=

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