International School on Rewriting - ISR'09

Universidade de Brasília, June 22-26, 2009

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 Knuth-Bendix completion can (sometimes) be used to make non-confluent term rewriting systems confluent. It can be used by the participants to acquaint or re-acquaint 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 first-order 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 alpha-equivalence and can be directly implemented. Nominal rewriting can be seen as a form of higher-order rewriting with a first-order syntax and built-in alpha-equivalence. Nominal systems maintain a strict distinction between atoms (variables that may be bound by a special abstraction operation) and meta-variables (or just variables) which cannot be bound, giving the framework a pronounced first-order character since substitution is not capture-avoiding. 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 first-order 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 (first-order) CTRSs
  • fundamental differences/difficulties/problems as compared to TRSs
  • confluence and (effective) termination properties: notions, (un)decidability, criteria, proof techniques
  • CTRSs and functional-logic programming
  • computatonal versus logical strength (logicality)
  • modularity in conditional rewriting
  • transformations from CTRSs to TRSs: soundness, completeness
  • expressiveness of CTRSs as compared to TRSs

    Fairouz Kamareddine (Heriot-Watt University)
  • 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)


    Delia Kesner (Université Paris Diderot (VII)) - Higher-order Rewriting with Resources (Track B)

    Higher-order 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 meta-level operation called higher-order substitution. This operation has been deeply studied in the framework of the lambda-calculus which can be seen as a paradigmatic example of higher-order rewriting system. Different lambda-calculi with explicit resources (contraction, weakening and substitution) were developed in order to internalise/implement the complex notion of meta-level 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 lambda-calculus with explicit substitutions and Multiplicative Exponential Linear Logic Proof-Nets 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
  • match-bounds
  • semantic labeling
  • derivational complexity
  • decidable classes

    Hitoshi Ohsaki (AIST)
  • Introduction to Tree Automata (Track A)
  • In 1960's tree automata originated as tree acceptors branched from context-free 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, sub-typing in programming language and formula manipulation of decidable second-order logics. In the course, first we review the classical (word) automata. We then introduce the concept of bottom-up tree automata, as a natural extension of word automata, and as a sub-class of ground rewriting, specifically, each of whose rewrite rules is formed of either f(p1, -> 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 1-3 in my lecture note.

  • Equational Tree Automata (Track B)
  • It is known that tree automata are closely related to context-free grammar, in fact, the leaf language of trees accepted by a regular tree automaton is a context-free language, and conversely, the set of derivation trees generated by a context-free 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, semi-linear 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 semi-linear 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 lambda-calculus. The majority of real functional languages have a "call-by-value" parameter passing policy, while the reduction rule of lambda-calculus reflects a "call-by-name" policy. In the folklore there was the idea that a call-by-value behavior could be mimicked in lambda-calculus just by defining a suitable reduction strategy. Plotkin proved that this intuition was wrong and that lambda-calculus is intrinsically call-by-name. So, in order to describe the call-by-value evaluation, he proposed a different calculus, which has the same syntax as lambda-calculus, but a different reduction rule. The parametric lambda-calculus has the same syntax of lambda-calculus and it is endowed by a reduction rule parametric with respect to a subset Delta of lambda-terms (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 call-by-value lambda-calculus. The most interesting feature of parametric lambda-calculus is that it is possible to prove important properties (like confluence) for a large class of languages in just one step. Thus the parametric lambda-calculus can be seen as the foundation of functional programming. We present the parametric lambda-calculus together with some of its main syntactical and semantic properties, on which their status of paradigmatic programming languages is based. Indicative Content Summary: parametric lambda-calculus, confluence, standardization, operational semantics and theories, other gadgets (computational power, separability, models).

    Organizing Committee

    Flávio L. C. de Moura Brasília, Brazil
    Mauricio Ayala-Rincó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

  • Sponsors: