
Rewriting is an important branch of theoretical
computer science which combines elements of logic and
mathematics. The Fourth International School on
Rewriting (ISR'09) will be held at Universidade de
Brasília, the week
before RDP'09, the
Federated Conference on Rewriting, Deduction, and
Programming. The school is organized for Master and
PhD students, researches and practitioners interested in
the study of rewriting concepts and applications. In
addition, the school is divided in two tracks (A and B)
in order to accommodate the different backgrounds of the
participants. The courses allocated on track A are for
the participants without previous exposure to rewriting,
while the courses on track B are advanced lectures on
recent developments and applications.
The lectures will be given by some of the
best experts on rewriting and applications.
The following
lecturers have been confirmed:
Franz
Baader (TU Dresden)  Introduction
to Term Rewriting (Track A)
Term rewriting systems can be used to compute in structures that are
defined by equations. They are thus an important tool in automated
deduction, algebraic specification, and functional programming. The
course introduces important properties such as termination and
confluence of term rewriting systems, describes methods for proving
termination and confluence, and shows how KnuthBendix completion can
(sometimes) be used to make nonconfluent term rewriting systems
confluent. It can be used by the participants to acquaint or
reacquaint themselves with the basic notions and results from the
area before taking more specialized or advanced courses.
Maribel
Fernandez (King's College London) 
Nominal Rewriting (Track B)
Nominal rewriting is a generalisation of firstorder rewriting that
allows us to deal with terms involving binding operators in an elegant
and practical way. In the nominal approach, bound entities are
explicitly named (rather than using a nameless syntax such as de
Bruijn indices), yet we get a rewriting formalism that respects
alphaequivalence and can be directly implemented. Nominal rewriting
can be seen as a form of higherorder rewriting with a firstorder
syntax and builtin alphaequivalence. Nominal systems maintain a
strict distinction between atoms (variables that may be bound by a
special abstraction operation) and metavariables (or just variables)
which cannot be bound, giving the framework a pronounced firstorder
character since substitution is not captureavoiding. In the course,
we will introduce the nominal approach to the specification of systems
with binding operators, and we will show how good properties of
firstorder rewriting are inherited by the nominal rewriting
framework. We will describe an efficient matching algorithm that has
been used to implement a nominal rewriting tool.
Bernhard
Gramlich (TU Wien)  Advanced
Course on Conditional Rewriting (Track B)
Conditional Term Rewriting Systems (CTRSs) extend ordinary Term
Rewriting Systems (TRSs) by allowing conditions in rewrite
rules. This is a very natural and conceptually adequate extension of
basic term rewriting. Although in many examples, from a purely
computational point of view, conditions in rewrite rules can be
avoided by an appropriate encoding within an unconditional framework,
the resulting encodings are not easy to understand and to analyze. For
that reason conditional term rewriting as such has been studied for a
long time, with the goal of extending the basic elegant and rich
theory of unconditional term rewriting to the conditional case as much
as possible. Yet, it has turned out that many results, approaches,
techniques and computational properties do not carry over easily, but
need to be carefully adapted to make sense. In the course, starting
with a thorough discussion of the basic notions and fundamental
problems in conditional rewriting, a selection of the following
topics will be covered (including exercises):
basic format, types, classes and notions of (firstorder) CTRSs
fundamental differences/difficulties/problems as compared to TRSs
confluence and (effective) termination properties: notions,
(un)decidability, criteria, proof techniques
CTRSs and functionallogic programming
computatonal versus logical strength (logicality)
modularity in conditional rewriting
transformations from CTRSs to TRSs: soundness, completeness
expressiveness of CTRSs as compared to TRSs
Traditional and non Traditional Typed λcalculi (Track A)
TBA
Extensions of Typed λcalculi with
Applications in Logic, Programming Languages and Formalisation
of Mathematics (Track B)
TBA
Delia Kesner
(Université Paris Diderot (VII))
 Higherorder Rewriting with
Resources (Track B)
Higherorder rewriting can be understood as a formalism allowing the
transformation of terms with bound variables. Different formalisms
exist to specify such transformations, all of them are based on a
metalevel operation called higherorder substitution. This operation
has been deeply studied in the framework of the lambdacalculus
which can be seen as a paradigmatic example of higherorder rewriting system.
Different lambdacalculi with explicit resources (contraction,
weakening and substitution) were developed in order to
internalise/implement the complex notion of metalevel
substitution. The course will survey research in the area of calculi
with explicit resources, by putting emphasis on motivations, history,
formalisms and properties. A formal correspondence between
lambdacalculus with explicit substitutions and Multiplicative
Exponential Linear Logic ProofNets will be established.
Aart
Middeldorp (Universität Innsbruck) 
Advanced Topics in Termination (Track B)
The course aims to give an impression of the state of the art
in termination research. The focus will be on methods that are
implemented in modern termination tools. The following topics
will be covered:
polynomial interpretations over various domains
matrix and arctic interpretations
dependency pairs
matchbounds
semantic labeling
derivational complexity
decidable classes
Introduction to
Tree Automata (Track A) In 1960's tree automata
originated as tree acceptors branched from contextfree grammar.
Over the decades since then, tree automata techniques have been
developed as a theoretical tool reasoning about questions over
trees in various areas, such as for protocol analysis, subtyping
in programming language and formula manipulation of decidable
secondorder logics. In the course, first we review the classical
(word) automata. We then introduce the concept of bottomup tree
automata, as a natural extension of word automata, and as a
subclass of ground rewriting, specifically, each of whose rewrite
rules is formed of either f(p1,...pn) > q or p > q, where f is a
function symbol and others are special constants, called "states."
Related properties including Pumping lemma, closure properties and
decidability are also explained as a counterpart of ones in word
automata. This lecture is based on Sections 13 in
my
lecture note.
Equational Tree Automata (Track
B) It is known that tree automata are closely
related to contextfree grammar, in fact, the leaf language of
trees accepted by a regular tree automaton is a contextfree
language, and conversely, the set of derivation trees generated by
a contextfree grammar is a tree language accepted by a (regular)
tree automaton. But, therefore, tree encoding by tree automata is
no longer powerful enough to express commutative languages,
semilinear sets or linear arithmetic. It turns out that in tree
languages, equational (for example, associative and/or
commutative) closure of regular tree languages are no longer
handled by tree automata. The course focuses on equational tree
languages (tree languages modulo equational theory) and related
topics. We learn the concept of equational tree automata, in
particular, in the two cases of AC theory and A theory. The course
also surveys the concept of commutative grammars and related
topics including Parikh's theorem for semilinear sets. This
course is based on Sections 7 and 8 in
my
lecture note.
Luca Paolini
(Università di Torino) 
Parametric Lambda Calculus (Track B)
There is a gap between real functional programming languages and
lambdacalculus. The majority of real functional languages have a
"callbyvalue" parameter passing policy, while the
reduction rule of lambdacalculus reflects a "callbyname" policy.
In the folklore there was the idea that a callbyvalue behavior could
be mimicked in lambdacalculus just by defining a suitable reduction
strategy.
Plotkin proved that this intuition was wrong and that lambdacalculus
is intrinsically callbyname. So, in order to describe the
callbyvalue evaluation, he proposed a different calculus, which has
the same syntax as lambdacalculus, but a different reduction rule.
The parametric lambdacalculus has the same syntax of lambdacalculus
and it is endowed by a reduction rule parametric with respect to a
subset Delta of lambdaterms (called the set of input values) that
enjoy some suitable conditions.
Different choices of Delta allow us to define different calculus,
in particular both classical and callbyvalue lambdacalculus.
The most interesting feature of parametric
lambdacalculus is that it is possible to prove important properties
(like confluence) for a large class of languages in just one step.
Thus the parametric lambdacalculus can be seen
as the foundation of functional programming.
We present the parametric lambdacalculus together with some of its main
syntactical and semantic properties, on which their status of
paradigmatic programming languages is based.
Indicative Content Summary: parametric lambdacalculus, confluence,
standardization, operational semantics and theories,
other gadgets (computational power, separability, models).
Organizing
Committee
Flávio L. C. de Moura 
Brasília, Brazil 
Mauricio AyalaRincón 
Brasília, Brazil 
Alberto Pardo 
Montevideo, Uruguay 
Eduardo Bonelli 
Buenos Aires, Argentina 
Steering Committee
Jürgen Giesl 
Aachen 
Claude Kirchner 
Bordeaux 
Pierre Lescanne 
Lyon 
Christopher Lynch 
Potsdam 
Aart Middeldorp 
Innsbruck 
Femke van Raamsdonk 
Amsterdam 
Yoshihito Toyama 
Sendai 
Previous editions of ISR
ISR'06
ISR'07
ISR'08
