[Termtools] Concerning certified competition.

[Claude Marché]

>>>>> "Adam" == Koprowski, A <A.Koprowski at tue.nl> writes:

    >>> [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?
    Adam>  You are right, part (2) should take a fraction of a second. So now, let
    Adam> me make sure that I do understand. You want parts:
    Adam>  (1) "runme": termination tool tries to find a certificate
    Adam>  (2) "checkme": translates this certificate to Coq script and runs Coq
    Adam> to verify it.
    Adam>  So essentially (2) and (3) from "Nancy proposal" are merged and it's
    Adam> participant's script that calls Coq and not the organizers. Correct?

YES


-- 
Claude Marché                          | tel: +33 1 72 92 59 69           
INRIA Futurs - ProVal                  | mobile: +33 6 33 14 57 93 
Parc Orsay Université - ZAC des Vignes | fax: +33 1 74 85 42 29   
3, rue Jacques Monod - Bâtiment N      | http://www.lri.fr/~marche/
F-91893 ORSAY Cedex                    |