The Coq mailing list

[Frederic Blanqui <frederic.blanqui AT inria.fr>]

Dear Christian,

please find more information about the current Coq termination checker 
in Bruno Barras presentation on 
http://coq.inria.fr/adt/egalite-terminaison .

Frederic.

Le 13/04/2011 04:50, Christian Doczkal a écrit :
> Dear Georges Gonthier, dear Coq-Club
>
> First of all, thank you for your quick reply. The paper [1], to which I
> was referring, defines a syntactic "guarded by destructors" condition
> for fix. As far as I can tell, this condition does not handle the case
> of div/mod. However, there appears to be an extended version in the form
> of an LIP research report that I was unable to obtain.
>
> I found a later paper from Giménez [2], where termination of fix is
> ensured by typing conditions. The paper employs guarded types and an
> order relation on types. The motivating example in this paper is a
> structurally recursive version of div.
>
> Now I'm curious whether Coq uses a type based approach for termination
> checking as proposed in [2] or a syntactic condition closer to [1],
> extended to cover div/mod. The Coq manual only references [1].
>
> I would be thankful for any clarification.