RTA'05

---

Yoshihito Toyama
Confluent Term Rewriting Systems

The confluence property is one of the most important properties of term rewriting systems, and various sufficient criteria for proving this property have been widely investigated. A necessary and sufficient criterion for confluence of terminating term rewriting systems, in which every reduction must terminate, was demonstrated by Knuth and Bendix (1970). For non-terminating term rewriting systems, Rosen (1973) proved that left-linear and non-overlapping term rewriting systems (i.e., no variable occurs twice or more in the left-hand side of a rewriting rule and two left-hand sides of rewriting rules must not overlap) are confluent, and the non-overlapping limitation was somewhat relaxed by Huet (1980), Toyama (1988), and van Oostrom (1997). However, few criteria have been proposed for confluence of term rewriting systems that are non-left-linear and non-terminating. Thus, it is still worth while extending criteria for these systems.

A powerful technique for showing confluence of a non-left-linear non-terminating term rewriting system is a divide-and-conquer method based on modularity by Toyama (1987) or persistency by Zantema (1994), Aoto and Toyama (1997). The method guarantees that if the system is decomposed into small subsystems and each of them is confluent then this system has the confluence property. Another useful technique is a transformational method based on conditional-linearization by Klop and de Vrijer (1991), Toyama and Oyamaguchi (1994), or a labelling technique. In this method we apply a non-confluence preserving transformation on a term rewriting system. Then the term rewriting system is confluent if the transformed system is confluent, because of non-confluence preserving. In this talk we will illustrate these techniques through various examples and discuss the relation among them.

---

Philip Wadler
Call-by-Value is Dual to Call-by-Name Reloaded

The rules of classical logic may be formulated in pairs corresponding to De Morgan duals: rules about "and" are dual to rules about "or". Wadler (2003), inspired by Curien and Herbelin (2000), presents a dual calculus in which exchanging "and" with "or" in types also exchanges call-by-value with call-by-name in evaluations. Just as the lambda calculus (of Church 1932,1940) corresponds to the intuitionistic natural deduction (of Gentzen 1935), the dual calculus corresponds to the classical sequent calculus (also of Gentzen 1935). This talk describes dual calculus, discusses its relationship to the mu calculus of Parigot (1992) and the Symmetric Lambda Calculus of Barbanera and Berardi (1996), and suggests further directions of research that may be of interest to the rewriting community.

---

Amy Felty
A Tutorial Example of the Semantic Approach to Foundational Proof-Carrying Code
joint invited talk with TLCA

Proof-carrying code provides a mechanism for insuring that a host, or code consumer, can safely run code delivered by a code producer. The host specifies a safety policy as a set of axioms and inference rules. In addition to a compiled program, the code producer delivers a formal proof of safety expressed in terms of those rules that can be easily checked. Foundational proof-carrying code (FPCC) provides increased security and greater flexibility in the construction of proofs of safety. Proofs of safety are constructed from the smallest possible set of axioms and inference rules. For example, typing rules are not included. In our semantic approach to FPCC, we encode a semantics of types from first principles and the typing rules are proved as lemmas. In addition, we start from a semantic definition of machine instructions and safety is defined directly from this semantics. Since FPCC starts from basic axioms and low-level definitions, it is necessary to build up a library of lemmas and definitions so that reasoning about particular programs can be carried out at a higher level, and ideally, also be automated. In this talk, I will describe a high-level organization that allows Hoare-style reasoning about machine code programs. This organization will be presented using a detailed example. The example, as well as illustrating the above mentioned approach to organizing proofs, is designed to provide a tutorial introduction to as many facets of our FPCC approach as possible. For example, it illustrates how to prove safety of programs that traverse input data structures as well as allocate new ones.

---

---

Gerard Huet
Before RTA: Early Days in Rewriting Research

We present a short overview of the early days in the development of rewriting theory, from 1970 to 1985, illustrated with personal experiences and collaborations.

---

Jean-Pierre Jouannaud
Twenty Years Later

The first RTA conference took place in Dijon, in 1985. This year, 2005, it takes place in Nara. Nara and Dijon share a glorious past but can be considered as being ``Sleeping Beauties'', after the title of a book by the Nobel price novelist yasunari Kawabata. Can we say that RTA has a glorious past ? Back in the late 80s, many of us feared that this would soon be the case. At that time, I felt that research in rewrite systems was deepening the gap with everyday's computer science pratice. Many of us thought that we should develop rewrite-based powerful provers that would make a difference with the state of art and help address real application such as software verification. More than ten years later this has not really happened in the way we thought it would. What has happened is that many research areas, such as programming languages, constraint solving, first-order provers, proof assistants, security theory, and verification have all been fertilized by ideas coming from our field. In return, our field has been renewed by new problems and techniques coming from outside our small community. I am convinced that this will continue, and that new subject areas will join the journey. There are at least two reasons. To quote a celebrated sentence that I have read in many papers, including in one by Nachum Dershowitz and myself, ``Equations are ubiquitous in computer science''. This is the first reason : we all like to use equations for modelling problems. The second is that we have developped extremely powerful, sophisticated tools to reason with equations. Many computer scientists do not know these tools. It is our responsibility to show them what we have done, and what we can do with it.

---

Nachum Dershowitz
Open Closed Open

We recount the history and geography of a selection of challenging closed and open problems in the theory of rewriting - as well as contemplate their future evolution and impact.

---