[Termtools] Upcoming competition - discussion during Nancy Workshop

[Xavier Urbain]

Hi all,

A few remarks,

First of all I am a bit surprised that such a discussion related to
the competition did not occur on the termtool list in first place.


> 4) Discussion on "checkme".
> 
> 4.1 The current rules (as written) would allow dummy checkme
> executables that just print "TRUE". This is not intended.  To make
> this intention more clear, the following is suggested (by all
> participants): "checkme" should in fact be "generate": it reads a
> proof and produces an input file for some established proof checker,
> possibly referring to some established libraries.  This input file
> shall be made visible on the competition web site.  The organizer
> (not the "checkme") then calls the proof checker on that file.

I don't see the point in reading a proof before generating. What if a
prover produce directly a checkable proof ?


> (For this year, we expect that all participants use Coq and CoLoR.

Could we have more information on this point?

Best regards,

Xavier


--

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

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