RTA'05

16th International Conference on Rewriting Techniques and Applications
April 19 - 21, 2005 Nara, Japan

PROGRAM OF RTA 2005

Tuesday (April 19)

8:30 - 9:00	Registration

9:00 - 10:00	Confluent Term Rewriting Systems (INVITED TALK)
	Yoshihito Toyama

10:00 - 10:20	Coffee Break

10:20 - 10:45	Generalized Innermost Rewriting
	Jaco van de Pol and Hans Zantema
10:45 - 11:10	Orderings for Innermost Termination
	Mirtha-Lina Fernandez, Guillem Godoy, and Albert Rubio
11:10 - 11:35	Leanest Quasi-Orderings
	Nachum Dershowitz and E. Castedo Ellerman

11:35 - 11:55	Coffee Break

11:55 - 12:20	Abstract Modularity
	Michael Abbott, Neil Ghani, and Christoph Lüth
12:20 - 12:45	Union of Equational Theories: An Algebraic Approach
	Piotr Hoffman

12:45 - 14:00	Lunch

14:00 - 14:25	Equivariant Unification
	James Cheney
14:25 - 14:50	Faster Basic Syntactic Mutation with Sorts for Some Separable Equational Theories
	Christopher Lynch and Barbara Morawska
14:50 - 15:15	Unification in a Class of Permutative Theories
	Thierry Boy de la Tour and Mnacho Echenim

15:15 - 15:35	Coffee Break

15:35 - 16:00	Dependency Pairs for Simply Typed Term Rewriting
	Takahito Aoto and Toshiyuki Yamada
16:00 - 16:25	Universal Algebra for Termination of Higher-Order Rewriting
	Makoto Hamana
16:25 - 16:50	Quasi-Interpretations and Small Space Bounds
	Guillaume Bonfante, Jean-Yves Marion, and Jean-Yves Moyen

16:50 - 17:10	Coffee Break

17:10 - 17:30	A Sufficient Completeness Reasoning Tool for Partial Specifications (System Description)
	Joe Hendrix, Manuel Clavel, and José Meseguer
17:30 - 17:50	Tyrolean Termination Tool (System Description)
	Nao Hirokawa and Aart Middeldorp
17:50 - 18:00	Report on the Termination Competition
	Claude Marché and Hans Zantema

18:00 - 18:20	Coffee Break

18:20 - 19:20	RTA Business Meeting

Wednesday (April 20)

9:00 - 10:00	Call-by-Value is Dual to Call-by-Name --- Reloaded (INVITED TALK)
	Philip Wadler

10:00 - 10:20	Coffee Break

10:20 - 10:45	Lambda-Mu-Calculus and Duality: Call-by-Name and Call-by-Value
	Jérôme Rocheteau
10:45 - 11:10	Reduction in a Linear Lamda-calculus with Applications to Operational Semantics
	Alex Simpson
11:10 - 11:35	Higher-Order Matching in the Linear Lambda Calculus in the Absence of Constants Is NP-Complete
	Ryo Yoshinaka

11:35 - 11:55	Coffee Break

11:55 - 12:20	Localized Fairness: a Rewriting Semantics
	José Meseguer
12:20 - 12:45	Partial Inversion of Constructor Term Rewriting Systems
	Naoki Nishida, Masahiko Sakai, and Toshiki Sakabe

12:45 - 14:00	Lunch

14:00 - 14:25	Natural Narrowing for General Term Rewriting Systems
	Santiago Escobar, José Meseguer, and Prasanna Thati
14:25 - 14:50	The Finite Variant Property: How to get rid of Some Algebraic Properties
	Hubert Comon-Lundh and Stéphanie Delaune
14:50 - 15:15	Intruder Deduction for AC-like Equational Theories with Homomorphisms
	Pascal Lafourcade, Denis Lugiez, and Ralf Treinen

15:15 - 15:35	Coffee Break

15:35 - 16:00	Proving Positive Almost-Sure Termination
	Olivier Bournez and Florent Garnier
16:00 - 16:25	Termination of Single-Threaded One-Rule Semi-Thue Systems
	Wojciech Moczydlowski and Alfons Geser
16:25 - 16:50	On Tree Automata that Certify Termination of Left-Linear Term Rewriting Systems
	Alfons Geser, Dieter Hofbauer, Johannes Waldmann, and Hans Zantema

16:50 - 17:10	Coffee Break


Anniversary Session - 20 Years of RTA: The History and Future of Rewriting

17:10 - 17:55	Before RTA: Early Days in Rewriting Research
	Gérard Huet
17:55 - 18:40	Twenty Years Later
	Jean-Pierre Jouannaud
18:40 - 19:25	Open. Closed. Open.
	Nachum Dershowitz

Thursday (April 21)

9:00 - 10:00	A Tutorial Example of the Semantic Approach to Foundational Proof-Carrying Code (INVITED TALK, joint with TLCA)
	Amy Felty

10:00 - 10:20	Coffee Break

10:20 - 10:45	Extending the Explicit Substitution Paradigm
	Delia Kesner and Stephane Lengrand
10:45 - 11:10	Arithmetic as a Theory Modulo
	Gilles Dowek and Benjamin Werner
11:10 - 11:35	Infinitary Combinatory Reduction Systems
	Jeroen Ketema and Jakob Grue Simonsen

11:35 - 11:55	Coffee Break

11:55 - 12:20	Proof-Producing Congruence Closure
	Robert Nieuwenhuis and Albert Oliveras
12:20 - 12:45	The Algebra of Equality Proofs
	Aaron Stump and Li-Yang Tan

12:45 - 14:00	Lunch

14:00 - 14:25	On Computing Reachability Sets of Process Rewrite Systems
	Ahmed Bouajjani and Tayssir Touili
14:25 - 14:50	Automata and Logics for Unranked and Unordered Trees
	Iovka Boneva and Jean-Marc Talbot

14:50 - 15:30	Coffee Break

15:00 - 17:30	Japanese Tea Ceremony / City Walk

17:30 - 20:30	Conference Dinner