| RTA 2004 15th International Conference on Rewriting Techniques and Applications |
 |
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 |