The Coq mailing list

[Eddy Westbrook <westbrook AT kestrel.edu>]

Bas,

Unfortunately, the 2011 technical report you cited of mine has some flaws in 
the proof. (Thanks to some of the members of this list that pointed them out 
in the past!) However, I am actually in the middle of trying to formalize a 
revised version of my proof in Coq itself.

One thing I have so far is what I think is a pretty general formalization of 
Coq. (I did look at the Coq in Coq project, but I think my approach is more 
general.) I define a term language, including all the universes of Coq, with 
an extensible notion of “operations” that are meant to capture inductive 
types, constructors, and recursors, as well as axioms like proof irrelevance, 
functional extensionality, etc., that I want to have interpretations in my 
model. I have done all the work for subject reduction, including a proof of 
confluence using superdevelopments (the operations are required to preserve 
superdevelopments). If anyone is interested, I can definitely share this. I 
would very much like some feedback on it.

Otherwise, I am still in the middle of building a model for this 
formalization — I am going to do the consistency proof first, and then extend 
it to SN — but if you or anyone else on the list is interested in seeing what 
I have so far, I would be happy to share it as well. I also have an updated 
write-up that sketches the ideas I am trying to use in my model construction. 
Again, the proof is not finished, so my approach could of course be flawed, 
but I am happy to share it as well, and would very much appreciate any 
feedback on it.

-Eddy

On Feb 28, 2016, at 10:15 AM, Bas Spitters 
<b.a.w.spitters AT gmail.com>
 wrote:

> 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