[Termtools] competition steering committee

[Johannes Waldmann]

Dear colleagues,

I have been elected to chair the competition steering committee.
(e-mail ballot among the current committee members,
votes collected by Aart). Thank you for your confidence.

(For completeness, I attach my "candidacy statement" below;
as it was mailed to the committee, but not to the list)


I intend to use this mailing list (termtools)
as the main discussion forum for all matters related
to the termination competition and database.
Input is welcome from everyone (not just committee).

The role of the committee is to vote on specific issues,
and role of the chair is to announce those votings,
collect and publish the results.

The committee currently consists of:
Jörg Endrullis, Jürgen Giesl, Dieter Hofbauer, Salvador Lucas,
Aart Middeldorp, Etienne Payet, Olivier Pons, Johannes Waldmann,
Hans Zantema.



#########################################################################################

( September 10th 2007 )

Dear colleagues,

I would like to serve as a chair for the competition steering committee.

As suggested, I give a brief presentation of my goals.

Although I think the committee as a whole does the "steering",
and the chair's task is merely
to induce, moderate, and record the committee's discussion.
(Hans is doing a great job at this at the moment.)

My technical suggestion is that
1. all discussion is archived and open (that is, on the termtools list)
   (I think we already agreed on that during WST07)
2. we need a procedure for voting, and software that implements it.
   (I hope that Peter Schneider-Kamp can provide this
   within the "termination web site" he started working on.)
(as for (1.), I don't really understand why the present discussion
is "off-list" but I won't change it for now.)

The immediate short term challenge for the community is a smooth
transition to the "new" competition format that we agreed upon;
including a change in the local organizer/hosting institution,
and a change in the execution model (towards "ongoing").
I support the Innsbruck proposal. I discussed with the group,
and I am convinced they can implement this transition.

A more far-reaching issue is the future direction of the competition.
This is a matter of opinions. I suggest that
whoever is interested in some special direction (or a change),
makes a public proposal and a prototype implementation;
then this can be tested by the participants, and become
part of the competition. Of course the committee may choose
to endorse proposals it thinks important.
(We see this happen with the subject of "certified proofs",
and "functional programs".)


This is the end of my "candidacy speech"; below I will state two issues
(certification, control language) that I find important;
but (the degree and pace of) their adoption would be a committee
decision, as outlined above.

Indeed my long-term idea is that all tool output has to be certified
(only then the "output" is a "proof", and the "tool" is a "prover")
but this is perhaps more of a guideline than a fixed target.
I think it is important to continue the development of a common proof
format (that is independent of the prover and the verifier).

Besides full certification, such a format has several other advantages:
since it is a uniform representation of proofs,
it can be used as a basis for displaying and querying;
it would allow partially certified proofs (some parts of the proof
may rely on "axioms" that will be certified later);
and it would allow for "special tracks" of the competition (where only
proofs adhering to some pre-defined subset of the format are accepted).

Another point that I would love to see encouraged by the committe
is a uniform control language for provers
that would allow to specifially select modes of execution;
and also to plug in other (partial) provers.
This would allow for modular provers,
and hopefully  lower the entry barrier for the competition.

Johannes Waldmann, Leipzig.