[Termtools] Upcoming competition - discussion during Nancy Workshop

[Frederic Blanqui]

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.)

the color workshop was intended to discuss such an intermediate language. this 
is unfortunate that you didn't come.

we also took advantage of this meeting to discuss some aspects of the 
termination competition. and johannes very kindly sent a summary of the 
discussions to the termtools list.

> prover produce directly a checkable proof ?

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