07:30 | The conference bus leaves from Hotel Ibis Linz. |
07:50 | The conference bus leaves from Hauptplatz Linz. |
08:30-08:00 | Registration, opening. |
| Invited Talk. Sesion chair: Johannes Waldmann |
09:00-10:00 |
Verification Techniques for Cryptographic Protocols. (Slides) |
| Véronique Cortier. |
10:00-10:30 | Coffee break. |
| Session 1. Chair: Albert Rubio |
10:30-11:00 | Maximal Termination. |
| Carsten Fuhs, Jürgen Giesl, Aart Middeldorp, Peter Schneider-Kamp, René Thiemann and Harald Zankl. |
11:00-11:30 | Modular Termination of Basic Narrowing. |
| María Alpuente, Santiago Escobar and José Iborra. |
11:30-12:00 | Termination Proof of S-Expression Rewriting Systems with Recursive Path Relations. |
| Yoshihito Toyama. |
12:00-12:30 | Arctic Termination ... Below Zero. |
| Adam Koprowski and Johannes Waldmann. |
12:30-14:00 | Lunch. |
| Session 2. Chair: Hans Zantema |
14:00-14:30 | Deciding Innermost Loops. |
| René Thiemann, Jürgen Giesl and Peter Schneider-Kamp. |
14:30-15:00 | Innermost Reachability and Context Sensitive Reachability Properties are Decidable for Linear Right-Shallow Term Rewriting Systems. |
| Yoshiharu Kojima and Masahiko Sakai. |
15:00-15:30 | Usable Rules for Context-Sensitive Rewrite Systems. |
| Raul Gutierrez, Salvador Lucas and Xavier Urbain. |
15:30-16:00 | Coffee break. |
| Session 3. Chair: Pierre Lescanne |
16:00-16:30 | Nominal Unification from a Higher-Order Perspective. |
| Jordi Levy and Mateu Villaret. |
16:30-17:00 | Linear-Algebraic Lambda-Aalculus: Higher-Order, Encodings, and Confluence. |
| Pablo Arrighi and Gilles Dowek. |
17:00-17:30 | A Finite Simulation Method in a Non-Deterministic Call-by-Need Lambda-Calculus with letrec, constructors, and case. |
| Manfred Schmidt-Schauss and Elena Machkasova. |
17:30-18:00 | Encoding the Pure Lambda Calculus into Hierarchical Graph Rewriting. |
| Kazunori Ueda. |
18:15 | The conference bus leaves from Hagenberg to Linz (Hauptplatz, Hotel Ibis). |
08:00 | The conference bus leaves from Hotel Ibis Linz. |
08:20 | The conference bus leaves from Hauptplatz Linz. |
| Invited Talk. Session chair: Jürgen Giesl |
09:00-10:00 |
Present and Future of Proving Termination of Rewriting. (Slides) |
| Albert Rubio. |
10:00-10:30 | Coffee break. |
| Session 4. Chair: Ralf Treinen |
10:30-11:00 | Logics and Automata for Totally Ordered Trees. |
| Marco Kuhlmann and Joachim Niehren. |
11:00-11:30 | Closure of Hedge-Automata Languages by Hedge Rewriting. |
| Florent Jacquemard and Michael Rusinowitch. |
11:30-12:00 | Tree Automata for Non-Linear Arithmetic. |
| Naoki Kobayashi and Hitoshi Ohsaki. |
12:00-12:30 | Combining Equational Tree Automata Over AC and ACI Theories. |
| Joe Hendrix and Hitoshi Ohsaki. |
12:30-14:00 | Lunch. |
| Session 5. Chair: Maribel Fernandez |
14:00-14:30 | Functional-logic Graph Parser Combinators. |
| Steffen Mazanek and Mark Minas. |
14:30-15:00 | Reduction under Substitution. |
| Roel de Vrijer and Joerg Endrullis. |
15:00-15:30 | Term-graph rewriting via explicit paths. |
| Emilie Balland and Pierre-Etienne Moreau. |
15:30-16:00 | Coffee break. |
| Session 6. Chair: Bernard Gramlich |
16:00-16:30 | Dependency Pairs for Rewriting with Built-in Numbers and Semantic Data Structures. |
| Stephan Falke and Deepak Kapur. |
16:30-17:00 | A Needed Rewriting Strategy for Data-Structures with Pointers. |
| Rachid Echahed and Nicolas Peltier. |
17:00-17:45 | Presentation of RISC and Softwarepark. |
17:45-18:00 | Coffee break. |
18:15 | The conference bus takes the SCIEnce Training School participants from Hagenberg to Linz (Hauptplatz, Hotel Ibis). |
18:00-19:00 | RTA business meeting. |
20:00 | The conference bus leaves from Hagenberg to Linz, hotel Arcotel. |
20:30-23:00 | Conference dinner at Arcotel. |
23:00 | The conference bus leaves from Arcotel to Hagenberg. |
08:00 | The conference bus leaves from Hotel Ibis Linz. |
08:20 | The conference bus leaves from Hauptplatz Linz. |
| Invited Talk. Session chair: Christopher Lynch |
09:00-10:00 |
Fast Equational Reasoning with Waldmeister. (Slides) |
| Thomas Hillenbrand. |
10:00-10:30 | Coffee break. |
| Session 7. Chair: Joachim Niehren |
10:30-11:00 | Root-Labeling. |
| Christian Sternagel and Aart Middeldorp. |
11:00-11:30 | Proving Quadratic Derivational Complexities using Context Dependent Interpretations. |
| Georg Moser and Andreas Schnabl. |
11:30-12:00 | Normalization of Infinite Terms. |
| Hans Zantema. |
12:00-12:30 | On Normalisation of Infinitary Combinatory Reduction Systems. |
| Jeroen Ketema. |
12:30-14:00 | Lunch. |
| Session 8. Chair: Gilles Dowek |
14:00-14:30 | Revisiting Cut-Elimination: One Difficult Proof is Really a Proof. |
| Christian Urban and Bozhi Zhu. |
14:30-15:00 | Finer is better: Abstraction Refinement for Rewriting Approximations |
| Yohan Boichut, Roméo Courbis, Pierre-Cyrille Heam and Olga Kouchnarenko. |
15:00-15:30 | Combining Rewriting with Noetherian Induction to Reason on Non-Orientable Equalities. |
| Sorin Stratulat. |
15:30-16:00 | Coffee break. |
| Session 9. Chair: Aart Middeldorp |
16:00-16:30 | Confluence by Decreasing Diagrams Converted. |
| Vincent van Oostrom. |
16:30-17:00 | Diagram rewriting for orthogonal matrices: a study of critical peaks. |
| Yves Lafont and Pierre Rannou. |
17:00-17:30 | Effectively Checking the Finite Variant Property. |
| Santiago Escobar, Jose Meseguer and Ralf Sasse. |
19:00-22:30 | Trip to Linz. Pflasterspektakel 2008. |
22:30 | The conference bus returns from Linz to Hagenberg. The meeting place in Linz will be announced later. |