[Termination tools] Several issues

[Salvador Lucas]

Dear all,

Juergen Giesl wrote:

> But I agree that it would be even more interesting to compare tools
> which work via a translation with tools which work on LPs or CSRSs
> directly. 

Encouraging such kind of research is also interesting, in my opinion.

> > I would like to suggest adding a new category (or categories)
> > involving real (rule-based) programming languages like Maude,
> > Elan, or Haskell...
>
> I agree that would be very interesting, but first we need to make sure
> that there will be tools which can handle these languages.

Well; founding the category would also be a way to stimulate
the development of such tools :-) In many cases they could
more or less quickly arise as (loosely coupled) combinations
of already existing tools; we have recently developed a
termination analyser for Maude which works like that by
using the Maude interpreter itself to transform Maude programs
into (CS-)TRSs, and CiME and MU-TERM to obtain the
termination proofs... The systems remain completely
independent and they just cooperate to obtain the proof by
using middleware techniques (do you want to join? :-)

Of course, completely integrated approaches are also
interesting, but they can take much more time or effort...

Best regards,

Salvador.