RTA program

Sessions take place in auditorium 3 unless otherwise indicated.

Monday July 22nd

Monday's program is also available with abstracts or side by side with other meetings.

08:45-09:55  FLoC opening (joint with FME, LICS)
Room: auditorium 1
Chair: Moshe Vardi

08:45  Introduction and welcome
08:55  Natarajan Shankar, SRI International, USA
Invited talk: Little engines of proof

10:00-10:30  Session 1
Chair: Daniel J. Dougherty

10:00  Paul-André Melliès, U Paris VII, France
Axiomatic rewriting theory VI: Residual theory revisited

10:30-11:00  Refreshments

11:00-12:30  Session 2
Chair: Thérèse Hardin

11:00  Richard Kennaway, U East Anglia, UK; Zurab Khasidashvili, Bar-Ilan U, Israel; and Adolfo Piperno, U Rome I (La Sapienza), Italy
Static analysis of modularity of beta-reduction in the hyperbalanced lambda-calculus
11:30  Germain Faure, ENS Lyon, France and Claude Kirchner, LORIA Nancy, France
Exceptions in the rewriting calculus
12:00  Georg Struth, U Augsburg, Germany
Deriving focused lattice calculi

12:30-14:00  Lunch

14:00-15:30  Session 3
Chair: Ralf Treinen

14:00  Hiroyuki Seki, Nara Inst. of Science and Techn., Japan; Toshinori Takai, AIST, Japan; Youhei Fujinaka, Nara Inst. of Science and Techn., Japan; and Yuichi Kaji, Nara Inst. of Science and Techn., Japan
Layered transducing term rewriting system and its recognizability preserving property
14:30  Hitoshi Ohsaki and Toshinori Takai, AIST, Japan
Decidability and closure properties for computation on equational tree languages
15:00  Pierre Réty and Julie Vuotto, U Orléans, France
Regular sets of descendants by some rewrite strategies

15:30-16:00  Refreshments

16:00-16:30  Session 4
Chair: Aart Middeldorp

16:00  Johannes Waldmann, U Leipzig, Germany
Rewrite games

16:30-17:30  Business meeting
Chair: Aart Middeldorp

19:00-21:00  City Hall reception (joint with FME, LICS)
Room: City Hall

Tuesday July 23rd

Tuesday's program is also available with abstracts or side by side with other meetings.

09:00-10:30  Session 5
Chair: Femke van Raamsdonk

09:00  Paula Severi, U Turin, Italy and Fer-Jan de Vries, U Leicester, UK
An extensional Böhm model
09:30  Julien Forest, U Paris XI (Paris-Sud), France
A weak calculus with explicit operators for pattern matching and substitution
10:00  Chuck Liang, Hofstra U, USA and Gopalan Nadathur, U Minnesota, USA
Application paper: Tradeoffs in the intensional representation of lambda terms

10:30-11:00  Refreshments

11:00-12:30  Session 6
Chair: Jürgen Giesl

11:00  John C. Mitchell, Stanford U, USA
Invited talk: Multiset rewriting and security protocol analysis
12:00  David Déharbe, Federal U of Rio Grande do Norte, Brazil; Anamaria Martins Moreira, Federal U of Rio Grande do Norte, Brazil; and Christophe Ringeissen, LORIA Nancy, France
Improving symbolic model checking by rewriting temporal logic formulae

12:30-14:00  Lunch

14:00-15:30  Session 7
Chair: Bernhard Gramlich

14:00  Janis Voigtländer, Dresden U of Techn., Germany
Conditions for efficiency improvement by tree transducer composition
14:30  Martin Bravenboer and Eelco Visser, Utrecht U, The Netherlands
Application paper: Rewriting strategies for instruction selection
15:00  Olivier Bournez and Claude Kirchner, LORIA Nancy, France
Probabilistic rewrite strategies: Applications to ELAN

15:30-16:00  Refreshments

16:00-17:20  Session 8: Tool Demonstrations
Chair: Albert Rubio

16:00  Jaco van de Pol, CWI Amsterdam, The Netherlands
Tool demonstration: JITty: A rewriter with strategy annotations
16:20  Irène Durand, U Bordeaux I, France
Tool demonstration: Autowrite
16:40  Benoit Lecland and Pierre Réty, U Orléans, France
Tool demonstration: TTSLI: an implementation of tree-tuple synchronized languages
17:00  Sylvain Lippi, IML Marseille, France
Tool demonstration: in²: A graphical interpreter for interaction nets

19:30-22:30  Conference dinner (joint with FME, LICS)
Room: Restaurant Luftkastellet

19:30  Banquet
21:30  Martin Davis, U California-Berkeley, USA
Plenary talk: Alan Turing & the advent of the computer

Wednesday July 24th

Wednesday's program is also available with abstracts or side by side with other meetings.

09:00-10:30  Session 9
Chair: Christopher Lynch

09:00  Alfons Geser, NASA Langley, USA
Loops of superexponential lengths in one-rule string rewriting
09:30  Elias Tahhan-Bittar, U Simón Bolívar, Venezuela
Recursive derivational length bounds for confluent term rewrite systems
10:00  Salvador Lucas, Polytechnic U of Valencia, Spain
Termination of (canonical) context-sensitive rewriting

10:30-11:00  Refreshments

11:00-12:30  Session 10
Chair: Joachim Niehren

11:00  Franz Baader, Dresden U of Techn., Germany
Invited talk: Engineering of logics for the content-based representation of information
12:00  Witold Charatonik, MPI Saarbrücken, Germany and Jean-Marc Talbot, U Lille, France
Atomic set constraints with projection

12:30-14:00  Lunch

14:00-15:30  Session 11
Chair: Jerzy Marcinkowski

14:00  Jordi Levy, U Barcelona, Spain and Mateu Villaret, U Girona, Spain
Currying second-order unification
14:30  Daniel J. Dougherty, Wesleyan U, USA and Tomasz Wierzbicki, U Wroclaw, Poland
A decidable variant of higher order matching
15:00  Franz Baader, Dresden U of Techn., Germany and Cesare Tinelli, U Iowa, USA
Combining decision procedures for positive theories sharing constructors