[Termtools] Concerning certified competition.

[Koprowski, A.]

>> [Adam]
>> 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
> [Claude]
> May be I did not understand something: is there anything special in
> that part (2) other than just translate XML syntax into Coq syntax? In
> a previous mail, I was asking whether this part would take a
> significant amount of time: I guess it would not. I am right?
 You are right, part (2) should take a fraction of a second. So now, let
me make sure that I do understand. You want parts:
 (1) "runme": termination tool tries to find a certificate
 (2) "checkme": translates this certificate to Coq script and runs Coq
to verify it.
 So essentially (2) and (3) from "Nancy proposal" are merged and it's
participant's script that calls Coq and not the organizers. Correct?

> In the rules, the checkme script is just supposed to return 0 if check
> went OK, but nothing is said about its output. If there is interest, I
> can manage to record its output and make it available, just like the
> output of runme is, by clicking on the CPU time. Then, if you want to
> see the Coq certificate, you could just write a copy to the standard
> output. This can be done in a few lines of shell script.
  Sounds ok. Making output and libraries available is really essential,
because everybody interested should be able to rerun the verification
and convince oneself that it is sensible.

> No problem: just submit the sources and tell me how to compile
> them. Ideally, I'd like just to run "make" if possible.
 We'll try to make it as easy as possible.

  Cheers,
  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 
========================================================================