---------------------------------------------------------------- IFIP Working Group 1.6 on Term Rewriting Report of the annual meeting: July 18, 2008 (Hagenberg, Austria) Chair: Claude Kirchner Vice-Chair: Juergen Giesl Secretary: Laurent Vigneron Participants: M. Fernandez (invited), J. Giesl, P. Lescanne, C. Lynch, A. Middeldorp, V. van Oostrom, F. van Raamsdonk, M. Schmidt-Schauss, R. Treinen (invited), J. Waldmann (invited), H. Zantema ---------------------------------------------------------------------- Agenda: 1. Technical presentations 2. Reports and general discussion 3. Business meeting ---------------------------------------------------------------------- 1. Technical presentations * Johannes Waldmann: Certified Termination The goal is to have automated termination provers that output certificates for termination that can be verified by an established proof checker (e.g. Coq, Isabelle). The central design decision is that the certificate format is both independent of the termination prover that produces it, and of the proof checker that verifies it. There are several research groups working in that area. In the 2007 Termination Competition, we established the "Certified" category, with several entrants. We also established the "Workshop on Certified Termination" (Nancy 2007, Leipzig 2008), and the talk summarizes some results and discussions from these meetings, see also http://termination-portal.org/wiki/WScT08-Minutes-Certification. Work on certified termination also helps to advance other areas, e.g., the discussion on the modular structure of the certificates automatically leads to discussion on the modular structure of termination provers. There, the goal is to provide sub-provers as pluggable, re-usable components. This will lower the "entry barrier" for new researchers that want to start working in automated termination. * Maribel Fernandez: Nominal Matching and Alpha-Equivalence Checks * Chris Lynch: Cap E-Unification Given a set S of terms, Cap(S) is the set of all terms that can be formed by adding function symbols on top of elements of S. Given S and a term t, the Cap Unification problem is to find a substitution theta such that there is a term s in S with theta a unifier of s and t. We give a decision procedure for Cap Unification. We also consider Cap E-unification: the Cap Unification problem modulo an equational theory. We show that Cap E-unification is equivalent to the secrecy problem from cryptographic protocol analysis for an active intruder with a bounded number of protocol sessions, where the equational theory represents the intruder abilities. We show conditions where Cap E-Unification is decidable, using an extension of Basic Narrowing called Cap Narrowing. The traditional Dolev-Yao intruder abilities are covered by our decidability result. * Ralf Treinen: Symbolic Protocol Analysis for Monoidal Equational Theories or: How Algebra Helps to Solve Intruder Constraints We consider the design of automated procedures for analyzing the (in)security of cryptographic protocols in the Dolev-Yao model for a bounded number of sessions when we take into account some algebraic properties satisfied by the operators involved in the protocol. This leads to a more realistic model than what we get under the perfect cryptography assumption, but it implies that protocol analysis deals with terms modulo some equational theory instead of terms in a free algebra. The main goal of this talk is to set up a general approach that works for a whole class of so-called monoidal theories which contains many of the specific cases that have been considered so far in an ad-hoc way, e.g., exclusive or, Abelian groups, exclusive or in combination with the homomorphism axiom. We follow a classical schema for cryptographic protocol analysis which proves first a locality result and then reduces the insecurity problem to a symbolic constraint solving problem. This approach strongly relies on the correspondence between a monoidal theory E and a semiring Se_E which we use to deal with the symbolic constraints. We show that the well-defined symbolic constraints that are generated by reasonable protocols can be solved provided that unification in the monoidal theory satisfies some additional properties. The resolution process boils down to solving particular quadratic Diophantine equations that are reduced to linear Diophantine equations, thanks to linear algebra results and the well-definedness of the problem. Examples of theories that do not satisfy our additional properties appear to be undecidable, which suggests that our characterization is reasonably tight. This is joint work with Stephanie Delaune, Pascal Lafourcade, and Denis Lugiez. * Manfred Schmidt-Schauss: Semantics of Programming Languages Based on Small-Step Operational Semantics Observational semantics of deterministic and non-deterministic programming languages can be defined using their respective small-step operational semantics (rewrite semantics). In general this provides the coarsest congruence w.r.t. observations, and thus can be seen as a canonical semantics. We present several methods and techniques to prove correctness of program transformations: may- and must-convergence, corresponding context lemmas, complete sets of diagrams, and methods to prove correctness of translations between programming languages. We show that the basic methods can be adapted and successfully applied to rather different kinds of programming languages. ---------------------------------------------------------------------- 2. Reports and general discussion * Aart Middeldorp: ISR 2008 Status Report A report on the forthcoming International Summer School on Rewriting in Obergurgl (Austria) is given. * General discussion on the future of ISR - It is decided to have ISR 2009 in Brasilia (Brazil), in connection with RTA 2009. The organizer is Mauricio Ayala Rincon. - It is proposed to have ISR 2010 in Utrecht (The Netherlands). The organizer is Vincent van Oostrom. - There are several suggestions on revising the ISR bylaws and on determining the member of the ISR steering committee. Femke van Raamsdonk, Aart Middeldorp, and Juergen Giesl will prepare a revision of the bylaws and a suggestion for the new ISR steering committee and then send them to the members of the IFIP working group for discussion and approval. The suggestion is considered approved if the majority of the members responding are in favor of it. * Next meeting of the IFIP working group There are two suggestions for the next meeting: either in Brasilia in connection with RTA 2009, or in Leipzig in connection with the International Workshop on Termination. It is decided to follow the first suggestion, i.e., the next meeting will take place in Brasilia. There is also a proposal to reduce the length of the meeting to half a day. ---------------------------------------------------------------------- 3. Business meeting * It is decided that if possible, the three invitees of this meeting (Maribel Fernandez, Ralf Treinen, Johannes Waldmann) as well as Delia Kesner (who was invited at the last meeting) should also become members of the working group. But before, all current members of the working group should be contacted and asked whether they are still interested in being members. Only those that reply positively should remain members. Afterwards, the four new members should be invited to join the working group. ----------------------------------------------------------------------