coq-club AT inria.fr

Subject: The Coq mailing list

List archive

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

From: Stefan Monnier <monnier AT IRO.UMontreal.CA>
To: Helmut Brandl <helmut.brandl AT gmx.net>
Cc: coq-club AT inria.fr
Subject: Re: [Coq-Club] Proof on strong normalization of cic
Date: Wed, 03 Oct 2018 07:59:00 -0400
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=monnier AT IRO.UMontreal.CA; spf=Pass smtp.mailfrom=monnier AT iro.umontreal.ca; spf=None smtp.helo=postmaster AT pruche.dit.umontreal.ca
Ironport-phdr: 9a23:mZiivhayr3jXfWbYsalcVrz/LSx+4OfEezUN459isYplN5qZr82ybnLW6fgltlLVR4KTs6sC17KJ9fi4EUU7or+5+EgYd5JNUxJXwe43pCcHRPC/NEvgMfTxZDY7FskRHHVs/nW8LFQHUJ2mPw6arXK99yMdFQviPgRpOOv1BpTSj8Oq3Oyu5pHfeQpFiCa/bL9oMBm6sRjau9ULj4dlNqs/0AbCrGFSe+RRy2NoJFaTkAj568yt4pNt8Dletuw4+cJYXqr0Y6o3TbpDDDQ7KG81/9HktQPCTQSU+HQRVHgdnwdSDAjE6BH6WYrxsjf/u+Fg1iSWIdH6QLYpUjm58axlVAHnhzsGNz4h8WHYlMpwjL5AoBm8oxBz2pPYbJ2JOPZ7eK7WYNEUSndbXstJVyJPHJ6yYYgBD+QPP+lXoYbyqEcBoxalGQmsHfnixiNUinLs36A31fkqHwHc3AwnGtIDqGnarMnrO6ccS++1yrTDwzLEb/NQ3zf96ZbHcgo8qvyLWLJwdszRyU8uFwzblFWdso/rMS+M2OgXvWeV6O1gVeSzi249tQ5+uDyvyt0yh4TVn48YzE3P+yZhwIstONG1RlB3bcS6HJdMuCyWLZV6T8wjTm1ypio21KUKtYO1cSQU0pgr2QLTZvOdf4SW4B/vTvidLDhmiH9jZbmxnQy98VK6xe35TsS00EhFri5CktTUrnANzQHT5dSHSvRj5EuuxDeP1xzJ5uFZJEA0kqzbK4I7wrEujJUTtV7PETPsl0nuja+WcFsr+vSw5uj6bLjquIWQO5FohgzxKKgihMOyDOUiPgQQQWSX4eG826fi/U39TrVKlPo2kqzBvZDfIsQboKi5Aw5L3YY58Bu/Di2m0NMCkXkaKVJFfxSHj5TzO17QOv/4Ce2zjEi2nztz3fDJIqXhAonRLnjEiLruYbF961dFxAUvydBf+olbB6oaIPPzX0/xrMbXAgU4Mwyy2ebnCc9y2pkQWWKVUeelN/byvFuN+/5nCfOFYoMR8GL9Jvwg+uKoh2Uwn1MZVaaszd0RZWzuTdp8JEDMWmbhjN4HWUINuAw/Qfai3FiFVzhSamyafpgboAweD4S6F4rKQsaGqerSj2+AApRKazUeWRi3GnDyetDBAq9UMXPAEopaijUBEIOZZcok3BCquhX9zuM3fOvO/WsFsJXlyMJ47umVnhhgrGUoXfTY6HmESiRPpk1NXyU/hfAtgHZajGqm1q5kmfFREZp4zqERC1poBdvn1+V/TuvKdEfBc9OOEgv0Ws+7CjE8CN4w35kTZkF7B8+vhxSF1CP4W7I=

> 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

[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