RTA  2004

15th International Conference on Rewriting Techniques and Applications


June 3 - 5, 2004          Aachen, Germany
RTA



PROGRAM  (Karman-Auditorium, Lecture Hall Fo 2)



Thursday (June 3)

9:15 - 10:15
Termination Analysis of the Untyped Lambda-calculus (INVITED TALK)

Neil Jones


10:15 - 10:50
Coffee break


10:50 - 11:25
A type-based termination criterion for dependently-typed higher-order rewrite systems

F. Blanqui
11:25 - 12:00
Termination of S-Expression Rewriting Systems: Lexicographic Path Ordering for Higher-Order Terms

Y. Toyama


12:00 - 14:00
Lunch


14:00 - 14:35
Monadic Second-Order Unification is NP-Complete

J.Levy, M. Schmidt-Schauss, and M. Villaret
14:35 - 15:10
A certified AC matching algorithm

E. Contejean


15:10 - 15:45
Coffee break


15:45 - 16:10
Matchbox: a Tool for Match-Bounded String Rewriting (System Description)

J. Waldmann
16:10 - 16:35
TORPA: Termination of Rewriting Proved Automatically (System Description)

H. Zantema
16:35 - 17:10
Querying Unranked Trees with Stepwise Tree Automata

J. Carme, J. Niehren, and M. Tommasi
17:10 - 17:45
A Verification Technique Using Term Rewriting Systems and Abstract Interpretation

T. Takai


18:00 - 19:30
Guided city walk
20:00
Conference dinner



Friday (June 4)

9:15 - 10:15
Bigraphs, Link Graphs, Transitions and Nets (INVITED TALK)

Robin Milner


10:15 - 10:50
Coffee break


10:50 - 11:25
Rewriting for Fitch style natural deductions

H. Geuvers and R. Nederpelt
11:25 - 12:00
Efficient lambda evaluation with interaction nets

I. Mackie
12:00 - 12:15
The RTA-List of Open Problems

N. Dershowitz and R. Treinen


12:15 - 14:00
Lunch


14:00 - 14:35
Proving Properties of Term Rewrite Systems via Logic Programs

S. Limet and G. Salzer
14:35 - 15:10
On the Modularity of Confluence in Infinitary Term Rewriting

J.  G. Simonsen


15:10 - 15:45
Coffee break


15:45 - 16:10
MU-TERM: A Tool for Proving Termination of Context-Sensitive Rewriting (System Description)

S. Lucas
16:10 - 16:35
Automated Termination Proofs with AProVE (System Description)

J. Giesl, R. Thiemann, P. Schneider-Kamp, and S. Falke
16:35 - 17:10
An Approximation Based Approach to Infinitary Lambda Calculi

S. Blom
17:10 - 17:45
Böhm-Like Trees for Term Rewriting Systems

J. Ketema


18:00 - 19:00
RTA business meeting



Saturday (June 5)


9:15 - 10:15
Dependency Pairs Revisited (INVITED TALK)

Aart Middeldorp


10:15 - 10:50
Coffee break


10:50 - 11:25
Inductive Theorems for Higher-Order Rewriting

T. Aoto, T. Yamada, and Y. Toyama
11:25 - 12:00
The Joinability and Unification Problems for Confluent Semi-Constructor TRSs

I. Mitsuhashi, M. Oyamaguchi, Y. Ohta, and T. Yamada
12:00 - 12:25
A Visual Environment for Developing Context-Sensitive Term Rewriting Systems (System Description)

J. Matthews, R. B. Findler, M. Flatt, and M. Felleisen