[Termtools] Upcoming competition - discussion during Nancy Workshop

[Xavier Urbain]

On Mon, May 14, 2007 at 02:09:03PM +0200, Frederic Blanqui wrote:
> On Mon, 14 May 2007, Xavier Urbain wrote:
> 
> >I don't see the point in reading a proof before generating. What if a
> 
> we think that it is interesting to have an intermediate language for 
> "termination certificates" that any termination prover could output, 
> and from which any termination proof certifier (eg. rainbow) could 
> generate a full formal proof in some safe proof checker/assistant 
> (coq, isabelle/hol, etc.)

I understand what is such a language and what can be obtained from it,
btw you know we are designing one.  Still I see no point in making a
rule of it.


> we also took advantage of this meeting to discuss some aspects of the 
> termination competition.

These aspects should be discussed on the relevant list, let's thank
Johannes for posting them.


> then, this is no problem for you: your checkme command has nothing to 
> do! :-)

Thus such a rule is useless, I see you agree. :-)

Best regards,

XU

-- 

Xavier Urbain
-----------------------------------------------------------------
CEDRIC, CPR

C.N.A.M. -- E.N.S.I.I.E.
-----------------------------------------------------------------