----------------------------------------------------------------
IFIP Working Group 1.6 on Term Rewriting
Report of the annual meeting: April 18, 2005 (Nara, Japan)
Chair: Claude Kirchner
Secretary: Laurent Vigneron
Participants: S. Anantharaman, H. Comon-Lundh, N. Dershowitz,
J. Giesl, B. Gramlich, G. Huet, T. Ida, D. Kesner (invited),
C. Kirchner, H. Kirchner, S. Lucas, N. Marti Oliet (invited),
J. Meseguer, A. Middeldorp, R. Nieuwenhuis, V. van Oostrom,
F. Pfenning (invited), P. Rety, Y. Toyama, L. Vigneron,
H. Zantema
----------------------------------------------------------------------
Agenda:
1. Progress Reports
2. Technical Presentations
3. General discussion: new trends in rewriting research and
applications
4. Business Meeting
----------------------------------------------------------------------
1. Progress reports
-----------------------------------------
* Narciso Marti Oliet: Rewriting-related research at DSIP-UCM.
Two groups related in rewriting:
- Declarative programming and TOY: domains are functional and logic
programming with constraints, and lazy narrowing with constraint
solving.
Recent results:
.Declarative debugging based on program transformation, embedded
into TOY.
.Constructive finite failure, operational procedures using failure
constructs, based on set narrowing.
.A new generic scheme for CFLP (constraint functional logic
programming over a constraint domain given as parameter).
- Rewriting logic and Maude:
.ITP: inductive theorem prover: to prove properties of membership
equational specifications.
.VLRL: a verification logic for rewriting logic.
-----------------------------------------
* Aart Middeldorp: Rewriting in Innsbruck.
Institute of Computer Science: created in 2001.
Holds 5 research groups, including the Computational Logic group
headed by Aart Middeldorp, with members: Stefan Blom, Georg Moser,
Nao Hirokawa, Christian Vogt.
Teaching: a 3 years bachelor program, 2 years master program (in
English), and a PhD program.
-----------------------------------------
* Tetsuo Ida: Activities of Foundations of Software Group at
University of Tsukuba.
Rewriting plays an important role at the university.
Related research topics:
- constraint solving and theorem proving: Origami construction and
geometrical theorem prover (Gröbner basis computation),
- symbolic computing grid: interaction of provers.
Many courses are related to rewriting, both in the College of
information science and in the Graduate school of systems and
information engineering.
-----------------------------------------
* Jose Meseguer: Progress report.
Topics studied:
- partial order reduction,
- narrowing with rules (for solving reachability problems),
- Maude language (with SRI and Madrid),
- modeling of programming languages (ex: Java),
- a tool environment for Maude,
- sufficient completeness,
- decision procedures for theorem provers,
- real-time specifications and systems,
- probabilistic rewriting.
Applications:
- model checking,
- pathfinder tool,
- networks security protocols.
----------------------------------------------------------------------
2. Technical Presentations
* The Dependency Pair Framework: Combining Techniques for Automated
Termination Proofs,
by Juergen Giesl.
Presentation of a general framework for combining (innermost)
termination techniques. It increases modularity, flexibility and
power. It encompasses the classical dependency pairs approach, and
facilitates the development of new termination techniques.
Illustration with a demonstration of AProVe, winer of the TRS
termination compatitions in 2004 and 2005.
* Some developments in proving termination automatically,
by Hans Zantema.
Presentation of three tools:
- TORPA, for string rewriting (uses advanced linear polynomials, a
transformation order and dummy elimination);
- TPA, for general term rewriting, using semantic labelling with
booleans and natural numbers;
- TEPARLA, for general term rewriting, using recursive labelling
with Booleans.
All three tools serve for proving relative termination, based on
polynomials and semantic labelling. Dependency pairs are only
partially used in the current versions.
* Term Rewriting in Pi-Calculus,
by Delia Kesner.
Relations between lambda calculus, higher-order rewriting and
first-order rewriting are put in evidence.
----------------------------------------------------------------------
3. New trends in rewriting research and applications
The discussion has permitted to raison some research points that
should be of strong interest in the next years:
- There is still a big gap between human intuition and automated tools
when considered the problem of verifying the termination of a
program.
-> how to transform a problem to make it easer to prove terminating?
- Verification machines are essential, but there are very few
higher-order proof systems.
- To work on the proof of non-termination or of non-correctness.
- There are still many difficult open problems: termination of
programs modulo some theories, sufficient confluence criteria,...
The tools written recently are not always easy of use, and are not
promoted with interesting examples:
- There is still a lack of effort for building systems accessible to
industrials (with a friendly interface, like Theorema), and able to
address real sized problems. For example, to study the termination
and the correctness of programs written in real programming
languages (Haskel, Java,...).
- There are more and more termination tools (from one to ten in three
years). To continue to design nice graphical interfaces. To use
more interesting examples.
- To provide real-life examples of use of rewriting.
Rewriting should be used in many domains:
- To do more efforts for linking rewriting with other domains, like
constraint solving. To contact/invite industrials and researchers
that could use rewriting.
- To be more present in committees, for having more weight in
promoting rewriting.
- There is no more big project for selling rewriting, and when there
is one (SLT, for example) people forget to use our expertise.
Concerning education, the points that have been raised are:
- Do we promote rewriting enough at school?
(logic is recognized as useful, and rewriting is logic...)
Isn't it learned too late? (this is the case in France for example)
- To build a European Master related to rewriting.
- To organize a summer school on rewriting.
- To emphasize the application of rewriting in courses titles (like
software verification), for attracting students.
- To push for the use of rule-based languages; they are more clear and
clean than any standard programming language.
----------------------------------------------------------------------
4. Business meeting
-----------------------------------------
* News from the IFIP:
- Election of the new TC1 Chair before the end of the year.
- TC1 meeting (sept 2004): activities of our group have been
presented.
The next TC1 meeting will hold in Chicago, just after the conference
LICS, in June 2005. Claude Kirchner will attend it.
-----------------------------------------
* Rewriting activities:
Past conferences and workshops:
- RTA 05: 79 submissions, 31 accepted papers, 131 participants.
- RULE 05: 27 participants.
-> RDP 05: 175 participants!
Rewriting lectures:
- ESSLLI 04: a one week course.
- Summer school on computational logic: Bernhard Gramlich will give
a course.
Upcoming workshops and conferences:
- The second workshop on Rewriting Calculus will be organized on May
30-31, 2005, at LIX (Paris-Palaiseau).
- RTA 06: August 12--15, 2006 (Seattle, USA).
- WRLA 06: March 25-26, 2006 (Vienna, Austria).
- RULE 06: August 11, 2006 (Seattle, USA).
- The second workshop on Rewriting Calculus will be organized in 2006
in London.
-----------------------------------------
* Information on the web:
A list of tools and lecture notes related to rewriting is available
at:
http://plateforme-qsl.loria.fr/Plate-forme QSL/
Members of the working group are encouraged to complete this list.
-----------------------------------------
* School on rewriting:
Pierre Lescanne and Femke van Raamsdonk made preliminary thoughts.
In any case it will hold in 2006, probably in summer.
A Steering Committee has to be built: the WG Chair will be a member,
as someone of the country where it will hold; additional volunteers:
Aart Middeldorp, Juergen Giesl.
-----------------------------------------
* Organization of the WG1.6 chairman election:
Claude Kirchner has been named WG Chair at the beginning of 2002.
So a new chairman has to be elected before the end of year 2005.
Nachum Dershowitz will organize the search for candidates and the
election (if possible before the end of the summer).
-----------------------------------------
* Next meeting:
In 2006, either in Seattle (FLoC), or during the summer school.
To check if it can be organized just before/after RTA at FLoC.
----------------------------------------------------------------------