Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] Guard Condition

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Guard Condition


chronological Thread 
  • From: Frederic Blanqui <frederic.blanqui AT inria.fr>
  • To: coq-club AT inria.fr
  • Subject: Re: [Coq-Club] Guard Condition
  • Date: Thu, 14 Apr 2011 09:18:57 +0800

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.





Archive powered by MhonArc 2.6.16.

Top of Page