---------------------------------------------------------------- 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. ----------------------------------------------------------------------