coq-club AT inria.fr

Subject: The Coq mailing list

List archive

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

From: Bas Spitters <b.a.w.spitters AT gmail.com>
To: Coq Club <coq-club AT inria.fr>
Subject: Re: [Coq-Club] Proof on strong normalization of cic
Date: Wed, 3 Oct 2018 07:31:12 +0200
Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=b.a.w.spitters AT gmail.com; spf=Pass smtp.mailfrom=b.a.w.spitters AT gmail.com; spf=None smtp.helo=postmaster AT mail-yb1-f173.google.com
Ironport-phdr: 9a23:CDbDUBdcZX62OztNt7rVDdy0lGMj4u6mDksu8pMizoh2WeGdxcS8Zx7h7PlgxGXEQZ/co6odzbaO7Oa4ASQp2tWoiDg6aptCVhsI2409vjcLJ4q7M3D9N+PgdCcgHc5PBxdP9nC/NlVJSo6lPwWB6nK94iQPFRrhKAF7Ovr6GpLIj8Swyuu+54Dfbx9HiTahY75+Ngm6oRnMvcQKnIVuLbo8xAHUqXVSYeRWwm1oJVOXnxni48q74YBu/SdNtf8/7sBMSar1cbg2QrxeFzQmLns65Nb3uhnZTAuA/WUTX2MLmRdVGQfF7RX6XpDssivms+d2xSeXMdHqQb0yRD+v9LlgRgP2hygbNj456GDXhdJ2jKJHuxKquhhzz5fJbI2JKPZye6XQds4YS2VcRMZcTyNOAo2+YIUPAeQPPvtWoZfhqFUBtha+GRCsCfnzxjNUmnP736s32PkhHwHc2wwgGsoDvWnOo9XuKawcTPi1zKjUzTXfcfxWwyz945XPfx86u/2DR6h8cMTLxUk0DwPFj0mQqZD7MDOPzeQAqGeb7+96WuKuj24rsR1+oj+qxso1jITCm4wbylfB9SpjwYY1I8W1SE99Yd6+EZtfrTuWN4VsQs86TGFouTo6yr0buZGgZiQF1JMnxxvHZ/yfdIiI5hLiVPqPLjhkhHJlfrO/hw+v8Ue+0OH8WNO03VBXpSRGitnBrm4B2wDX58SdSfZw/l2t1SiS2w3X8O1IPEI5mKTdJpU82LA/jIATvl7GHiLumEX5kquWdkI89+it8evnY7HmqoacNoBvlw3yK6oultG9DOk2KAQOUG+b+eOz1L3n40L1WqlFjvozkqXBsZDaI9oUprKhDgNLzoou7wyzAjSm3dgCg3ULMVZIdAiag4XrNVzCOPX4Au2+g1Sonjdr3ffGPrj5D5rWNHTMiq3tfLhn505H0AozzMxf545KBbEbO/L+QUDxtNnCAR84Nwy42froCNJ41o8GQ2KAHreZML/OsV+P/u8gP+6MZJYMtDnhL/gl+uXhgGQimV4deKmpxYEYZGq5HvRgOUWZYGDjjs0PEWcQ7UICS7nBj0TKejpObT7mVKUlozo/FYiODIHZR4nrjqbXjwmhGZgDTGldQmuUEGv0ep+fE6MGLivUPYl6ij0YSbW7UKcu0BivsEnxzL8xfbmcwTERqZ+2jIs93ObUjxxnsGUsV53MgVHIdHl9myYzfxFz2al+pUJnzVLaiPp3hvVZEZpY4PYbC15mZ66Z9PRzDpXJYiyEZs2AEQ/0TdCvADV3RdU0kYdXPhRNXu66hxWG5BKERr8Yk7vRWs4x+6PYmmn7foNzkimdkqYmiFYiT41EMmj03qM=

A bit of discussion is here:
https://github.com/coq/coq/wiki/CoqTerminationDiscussion
On Wed, Oct 3, 2018 at 5:38 AM Helmut Brandl
<helmut.brandl AT gmx.net>
wrote:
>
> 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