coq-club AT inria.fr

Subject: The Coq mailing list

List archive

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

From: "William J. Bowman" <wjb AT williamjbowman.com>
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: Tue, 2 Oct 2018 19:34:07 -0400
Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=wjb AT williamjbowman.com; spf=None smtp.mailfrom=wjb AT williamjbowman.com; spf=None smtp.helo=postmaster AT williamjbowman.com
Ironport-phdr: 9a23:s70cABIVi/3r29gBV9mcpTZWNBhigK39O0sv0rFitYgeIv3xwZ3uMQTl6Ol3ixeRBMOHs60C07KempujcFRI2YyGvnEGfc4EfD4+ouJSoTYdBtWYA1bwNv/gYn9yNs1DUFh44yPzahANS47xaFLIv3K98yMZFAnhOgppPOT1HZPZg9iq2+yo9JDffwdFiCChbb9uMR67sRjfus4KjIV4N60/0AHJonxGe+RXwWNnO1eelAvi68mz4ZBu7T1et+ou+MBcX6r6eb84TaFDAzQ9L281/szrugLdQgaJ+3ART38ZkhtMAwjC8RH6QpL8uTb0u+ZhxCWXO9D9QKsqUjq+8ahkVB7oiD8GNzEn9mHXltdwh79frB64uhBz35LYbISTOfFjfK3SYMkaSHJPUMhRSSJPH4Cyb4UAAOUdIOlWoIvyqFUVoBuiBgShHv/jxiNSi3L026AxzuQvERvB3AwlB98CvnTbrNTxNKcWUOC61qzIxijHYf9MxDzw9Y/Icx4kof6WW7J8f9faxE4hFgPHlVqdsoLkPzKR1uQJsmiU9e9gVeC0hG4gpQBxpyKgxsE2hobVgYIVz0nJ+CNky4g7It24TVR0Yd+iEJZItiGaMZF2QsI4TG1ytiY60KUKuYa8fCgOyJUn2wDQZOCHc4iO4xLjTfuRLiliiHJrYrKygQu5/0u4yuDkS8W51EhGojBYntTMtn0BzR/e58udRvdg40us2C6D2x3N5uxAO0w4iLbXJ4Q8zrItipYfq0vOEyzwlU7rlqGZbF8k9fKt6+n/YrXpuJucN4hshwDwM6Qunsi/AeUiPQgLXWiU4uO81bPm/ULjRrVGlOE5kq7csJzCJMQboLC2AxNN34o+7xuzES2q3MkYkHQHNl5IexGKg5L0N13TIf30FfK/jE6tkDdvyfDGJLrhApDVI3nNkrfuZq1w6kBdyAo3ydBf5ohbCrQDIP3oXU/wutnYAQU/MwCu3+nnD9B92psEWW2TGq+ZLL/SsViQ6+0zJOmMfZYZtyr5K/g4/PHjlmQ5mF8Yfamxx5QbcnG4HvJ8I0WYe3XgmNkBEX1Z9jY5GcznjFifTXZ5fX+0U6Z0sjE2DIe7EcHJXImrjLip0yKrWJtbejYVJEqLFCKiSISAX/YFbWqwZIdLlSMBXL7rA9s+1xuGqw7+z7tuK+je/TIdvJSl399wsb6A3Sou/CB5WpzOm1qGSHt5yyZRH2dvjfJP5Hdlw1LG6pBWxvlRFNhd/fRMCF9oKp/Yy+1zDtL4XR3Ed9HPQ1GjEI3/XWMBC+kpytpLWH5TXs24h0qbjTWrB7sUnrmJDpsr96vamXP2IpQlkiuU5Owal1AjB/B3Gyimi6p4rVCBGI/Nl0SQkqSgcrsZ1SiL/2CGnzKD

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