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