[Termtools] Concerning certified competition.

[Koprowski, A.]

>> [Johannes]

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

> [Claude]

> NO. the "runme" script should generate that. It can be any format,
such as the XML format expected from the Color project.

 

The idea discussed during the meeting at Nancy was as follows:

(1) "runme": runs the termination prover which produces a proof in some
format (like XML format of CoLoR)

(2) "checkme": reads that proof and translates it to a
Coq/Isabelle/PVS/... script

(3) organizers run Coq/Isabelle/PVS/... on the generated script to
verify it.

 

>> [Johannes] 

>> The organizer (not the "checkme") then calls the proof checker on
that file.

> [Claude]

> I do not understand: I will not run anything by hand!

 The idea of (3) being done by organizers was to makes this verification
explicit (and not part of a script provided by participants, which may
do whatever it desires, including something silly). Of course it should
be part of the script maintaining the competition and not done "by
hand".

 

 I think ideally both the intermediate result (XML/...) and the final
certificate (Coq/... script) should be available via the results page.
But the latter must necessarily be accessible for credibility of the
verification process.

 

> [Claude]

> Compiled before the competition: of course.

> But what does "installing" mean? Do you need Color installed in a
specific place? Why not in the same directory as the runme, > checkme,
etc.

 I think it's ok to provide CoLoR in a bundle, together with a
termination prover. It could even be precompiled, but then there are two
problems:

- the binaries of CoLoR are around 40MB,

- we would have to make sure that it's compiled with precisely the same
version of Coq as used during the competition, as otherwise the binaries
may be incompatible. 

  The preliminary round to check that everything is fine (as for other
categories) would be most welcome!

 

  Greetings,

   Adam

 

--

========================================================================

 Adam Koprowski, (A.Koprowski at tue.nl, http://www.win.tue.nl/~akoprows)

 Department of Mathematics and Computer Science

 Eindhoven University of Technology (TU/e)

 The difference between impossible and possible lies in determination

      Tommy Lasorda 

========================================================================

 

-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.lri.fr/pipermail/termtools/attachments/20070514/6d7c1386/attachment-0001.htm