[Termination tools] termination competition: certification of proofs

[Salvador Lucas]

Dear all,

Frederic Blanqui wrote:

> adam koprowski and i are going to design some xml format, and develop 
> some interface for coq/color. we will inform the termtools list when 
> it will be ready. 

After my WST'04 talk about connecting tools, Claude
asked me to develop an XML format which could be
appropriate for that purposes (which Hans somehow
put on the table again with his message yesterday).

After our recent experience in developing a tool for proving
termination of Maude programs by combining different
independent tools (namely, the Maude interpreter,
CiME and MU-TERM), I have discussed this
problem with people from the Maude group. We think
interesting to generalize the concrete treatment we did
(via Web services) by defining appropriate XML formats
which could be used with termination tools.

Probably we could, then, coordinate our effort or even
work together to design and develop an new XML
TPDB format where all the discussed aspects are
considered and smoothly integrated.

Best regards,

Salvador.