coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] Is Coq SN ?

From: Bas Spitters <b.a.w.spitters AT gmail.com>
To: Coq Club <coq-club AT inria.fr>
Subject: [Coq-Club] Is Coq SN ?
Date: Sun, 28 Feb 2016 19:15:09 +0100
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-wm0-f44.google.com
Ironport-phdr: 9a23:ymY8mRexfmHfJWJ2YvmNuzrQlGMj4u6mDksu8pMizoh2WeGdxc69YR7h7PlgxGXEQZ/co6odzbGG7Oa+BydZucvJmUtBWaIPfidNsd8RkQ0kDZzNImzAB9muURYHGt9fXkRu5XCxPBsdMs//Y1rPvi/6tmZKSV3BPAZ4bt74BpTVx5zukbvipNuNPU4R3Gf1SIgxBSv1hD2ZjtMRj4pmJ/R54TryiVwMRd5rw3h1L0mYhRf265T41pdi9yNNp6BprJYYAu3SNp41Rr1ADTkgL3t9pIiy7UGCHkOz4S43VXxeuR5VCUCR5xbjG5z1ryHSt+xn2SDcM9egHp4uXjH3xa5wACTwiTsbOiQiuDXdzMU2k+RAuBO9uxFl2KbbZYiUMLx1eaaLLoBSfnZIQssED38JOYi7dYZaSrNZZes=

Is Coq strongly normalizing?

The *implementation* of Coq is (or was) not SN. The issue is recorded
here, I believe.
https://coq.inria.fr/cocorico/CoqTerminationDiscussion

I am not sure whether this has been fully fixed yet.

The Coq manual is incomplete, as it refers to Coquand's work on CoC
for the SN proof of CIC, which can't be strictly right.
https://coq.inria.fr/refman/Reference-Manual006.html
I haven't chased the references yet, but this paper claims the result for CIC:
https://www.cs.rice.edu/research/technical-reports/TR11-01/

Does this seem correct? It would be probably be good to document this
properly (in the FAQ, ref manual?).

Bas

[Coq-Club] Is Coq SN ?, Bas Spitters, 02/28/2016
- Re: [Coq-Club] Is Coq SN ?, Maxime Dénès, 02/28/2016
  - Re: [Coq-Club] Is Coq SN ?, Abhishek Anand, 02/28/2016
    - Re: [Coq-Club] Is Coq SN ?, roux cody, 02/28/2016
      - Re: [Coq-Club] Is Coq SN ?, Luo, Zhaohui, 02/29/2016
        
        Re: [Coq-Club] Is Coq SN ?, Thorsten Altenkirch, 02/29/2016
        
        Re: [Coq-Club] Is Coq SN ?, Frédéric Blanqui, 02/29/2016
        
        Re: [Coq-Club] Is Coq SN ?, Thorsten Altenkirch, 02/29/2016
        Re: [Coq-Club] Is Coq SN ?, Thorsten Altenkirch, 02/29/2016
        
        Re: [Coq-Club] Is Coq SN ?, Frédéric Blanqui, 02/29/2016
        Re: [Coq-Club] Is Coq SN ?, roux cody, 02/29/2016