RDP  2004

Federated Conference on Rewriting, Deduction, and Programming

May 31 - June 5, 2004

Aachen, Germany

 RTA


PROGRAM
 
The preliminary program is shown in the following table. On Saturday (June 5), the program will only be in the morning.
May 31 June 1 June 2 June 3 June 4
 June 5
WG 1.6
 WST
 RTA
WFLP WRS
RULE
 HOR



City Walk
 RTA Business Meeting



RTA Conference Dinner



Monday, May 31:   IFIP WG 1.6  (Hotel IBIS Marschiertor)


Tuesday, June 1: WST, WFLP, RULE (Karman-Auditorium, Lecture Halls Fo 4, Fo 5, and Fo 8)

WST (Fo 4)
 WFLP (Fo 5) RULE (Fo 8)
9:20 - 9:30
Opening
 Opening
9:30 - 10:00

 Erasure and Termination in Higher-Order Rewriting TeaBag: A Functional Logic Language Debugger Playing with Maude
J. Ketema and F. van Raamsdonk S. Antoy and  S. Johnson M. Palomino, N. Marti-Oliet, and A. Verdejo
10:00 - 10:30
 Reducing the Constraints of the Dependency Pair Approach Constraint Solving for Generating Glass-Box Test Cases On-demand evaluation for Maude
J. Giesl, R. Thiemann, and P. Schneider-Kamp C. Lembeck, R. Caballero, R.A. Müller, and H.Kuchen F. Duran, S. Escobar, S. Lucas

10:30 - 11:15

 Coffee break
11:15 - 11:45

 Report on the Termination Competition A logical approach to the verification of functional-logic programs A Rewriting-based Framework for Web Sites Verification
C. Marché J.M. Cleva, J. Leach, and F.J. Lopez-Fraguas M. Alpuente, D. Ballis, and M. Falaschi
11:45 - 12:15

 MU-TERM: A Tool for Proving Termination of Rewriting with Replacement Restrictions TypeTool: A Type Inference Visualization Tool A Compiler for Mapping a Rule-Based Event-Triggered Program to a Hardware Engine
S. Lucas
 H. Simoes and  M. Florido C. Albrecht and A. Doering

12:15 - 14:00
Lunch


14:00 - 14:30

 INVITED TALK Dynamic Predicates in Functional Logic Programs Context-free Tree Languages for Descendants
M. Hanus P. Rety and J. Vuotto
14:30 - 15:00

 Encapsulating Non-Determinism in Functional Logic Computations A System Design for Associative and Commutative Tree Automata Theory: ACTAS
Danny de Schreye B. Braßel, M. Hanus, and F. Huch H. Ohsaki and T. Takai
15:00 - 15:30
 Abstract Partial Evaluation for Termination Analysis Comparing Copying and Trailing Implementations for Encapsulated Search Rule-based Programs describing Internet Security Protocols
L. Tamary and M. Codish W. Lux Y. Chevalier and L. Vigneron

15:30 - 16:15

 Coffee break
16:15 - 16:45

 Polynomials over the Reals in Proofs of Termination
 Symbolic Representation of tccp Programs Principles of Chemical Programming
S. Lucas M. Alpuente, M. Falaschi, and A. Villanueva J.-P. Banatre, P. Fradet, and Y. Radenac
16:45 - 17:15

 Natural Polynomial Interpretations A Fixed Point Semantics for an Extended CLP Language Strategy Construction in the Higher-Order Framework of TL
N. Hirokawa amd  A. Middeldorp M. Garcia-Diaz and S. Nieva V. Winter
17:15 - 17:25
Closing
 Closing




Wednesday, June 2: WST, HOR, WRS (Karman-Auditorium, Lecture Halls Fo 4, Fo 5, and Fo 8)

WST (Fo 4) HOR (Fo 5) WRS (Fo 8)
9:00 - 9:30
 Modularity of Termination of Left-Linear Rewrite Systems Revisited FD a la Mellies
B. Gramlich V. van Oostrom
9:30 - 10:00

 A Note on a Term Rewriting Characterization of PTIME Strong normalization in the rho-cube: the first-order system
 Reduction Cycles (INVITED TALK)
T. Arai and G. Moser B. Wack
10:00 - 10:30

 A Practical Approach to Proving Termination of Recursive Programs in Theorema Termination of simply-typed applicative term rewriting systems
N. Popov and  T. Jebelean T. Aoto and T. Yamada
 Jan Willem Klop

10:30 - 11:00

 Coffee break
11:00 - 11:30

 Proof-Theoretic Analysis of Lexicographic Path Orders
Higher-order rewriting via conditional first-order rewriting in the open calculus of constructions (INVITED TALK)
 Autowrite: a tool for term rewrite systems and tree automata
J.W. Klop, V. van Oostrom, and R. de Vrijer I. Durand
11:30 - 12:00

 Tree Automata that Certify Termination of Term Rewriting Systems Integrating Decision Procedures in Reflective Rewriting-Based Theorem Provers
A. Geser, D. Hofbauer, J. Waldmann, and  H. Zantema
 Mark-Oliver Stehr
 M. Clavel, M. Palonimo, and J. Santa-Cruz
12:00 - 12:30
 Relative Termination in Term Rewriting Unification and matching modulo type isomorphism
 Some Undecidable Approximations of TRSs
H. Zantema D. Dougherty and C. Martinez
 J. Ketema

12:30 - 14:00
Lunch


14:00 - 14:30

 Proving termination with AProVE Pure type systems, cut and explicit substitutions
 Normalization by Evaluation (INVITED TALK)
J. Giesl, R. Thiemann, P. Schneider-Kamp, and S. Falke R. Kervarc and P. Lescanne
14:30 - 15:00

 Tyrolean Termination Tool PSN implies SN
N. Hirokawa and  A. Middeldorp E. Polonovski
 O. Danvy
15:00 - 15:30

 Connecting Remote Termination Tools Deriving strong normalization
 Invariant-Driven Strategies
M. Alpuente and  S. Lucas S. Lengrand
 F. Duran and M. Roldan

15:30 - 16:00

 Coffee break
16:00 - 16:20
 Demo/Exhibition of Termination Tools


This event takes place
in Room SFo 1
 		Intersection Types and Lambda Models (INVITED TALK)

Mariangola Dezani 		DS-forest: A Data Structure for Fast Normalization and Efficiently Implementing Strategies (Position Paper)

R. Verma and J. Thigpen
16:20 - 17:00
 Round Table: Strategies in Programming Languages Today

F. Duran, C. Kirchner, and R. Laemmel
Moderator: S. Lucas
17:00 - 17:20
 Higher-order rewriting with types and arities

J.-P. Jouannaud, F. van Raamsdonk, and A. Rubio
17:20 - 17:30
 PC Meeting
17:30 - 18:00
 |_|

V. van Oostrom, K.-J. van de Looij, and M. Zwitserlood




Thursday, June 3:   RTA (Karman-Auditorium, Lecture Hall Fo 2)
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:   RTA (Karman-Auditorium, Lecture Hall Fo 2)
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:   RTA (Karman-Auditorium, Lecture Hall Fo 2)

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