The Coq mailing list

[Bas Spitters <b.a.w.spitters AT gmail.com>]

I am aware it comes up regularly. I was even in the bug-tracker at some point.
However, this information should be recorded. Thanks for your input.

Do you have a reference for WN ?

I have added very basic information here (for lack of a better place):
https://coq.inria.fr/cocorico/CoqTerminationDiscussion

On Thu, Dec 22, 2016 at 8:27 PM, roux cody 
<cody.roux AT gmail.com>
 wrote:
> As the discussed example (and the example discussed last week) shows,
> Gallina/Coq is *not* SN, though as far as we know it *is* WN, which is
> enough for consistency.
>
> This issue comes up regularly on the list, and I believe that the summary is
> as follows:
>
> - It's extremely difficult for the theory to keep up with the practical
> demands of the system.
> - We should be trying to have a reasonable meta-theory anyways.
> - There are a few papers which prove normalization of various fragments and
> variants of Coq. However, I know of none that handle CiC + Impredicative
> Prop + Universes + Large Elimination (don't even ask about impredicative
> set!). I can try to list them if required, but I always worry about
> forgetting a crucial one.
> - The above works are extremely technical and hard to fully check, this
> seems to be begging for a machine formalized proof.
> - Such a proof is extremely tough, given the technical complexities
> involved, and the Godelian meta-theoretical issues (certainly something will
> have to be assumed as an axiom).
>
> My constant call is for a more thorough exploration of the abstract
> structure of such proofs, so we can clearly separate it into combinatorial
> considerations + a model construction, which may be more tractable. There's
> a bunch of work on this as well, including the whole sub-field about
> normalization-by-evaluation, but CiC + universes seems a bit out of reach
> for now with such techniques, and again, writing down the whole construction
> is extremely tedious and error prone.
>
> Hope this helps give the high overview,
>
> Best,
> Cody
>
>
> On Thu, Dec 22, 2016 at 8:10 AM, Bas Spitters 
> <b.a.w.spitters AT gmail.com>
> wrote:
>>
>> This page refers to an example showing that Coq is not SN (due to the
>> guard condition).
>> https://coq.inria.fr/cocorico/CoqTerminationDiscussion
>>
>> However, this (unpublished) report claims that CiC (with Prop and
>> universes) is SN.
>>
>> http://csweb.rice.edu/uploadedFiles/Computer_Science/Research/Tech_Reports/TR11-01.pdf
>> Uniform Logical Relations - Eddy Westbrook
>>
>> Has there been any progress on this? It would be good to update the
>> wiki/FAQ with this information.
>
>