|Registration of Talks||Sunday, October 30|
|Participant registration||Sunday, November 6|
If you are interested in giving a talk or if you have any other questions regarding the organization of the meeting, please contact:
| Friday, November 18
|13:00||-||13:45||Application of a Prefix Property of Higher-Order Rewriting Systems to Finite Family Developments|
|Sander Bruggink, Universiteit Utrecht|
|13:45||-||14:30||Match-Bounded String Rewriting|
|Jörg Endrullis, Vrije Universiteit Amsterdam|
|15:00||-||15:45||Proving termination of string rewriting by matrix interpretations|
|Hans Zantema, TU Eindhoven|
|15:45||-||16:30||Disproving Termination of Term Rewriting|
|Jürgen Giesl, RWTH Aachen
|16:30||-||17:00||TeReSe business meeting|
|Sander Bruggink: Application of a Prefix Property of Higher-Order Rewriting Systems to Finite Family Developments|
A rewriting system has the prefix property, in its most general form, if it is the case that, given some rewrite step from s to t, the ancestor of a prefix of t is a prefix of s. In this talk I prove a prefix property for higher-order rewriting systems, by reducing the property to a prefix property for a lambda calculus with explicit substitutions, and use this result to prove finiteness of family developments.
|Jörg Endrullis: Match-Bounded String Rewriting|
| Hans Zantema: Proving termination of string rewriting by matrix interpretations
was an open problem until a few months ago when it was solved by Hofbauer and Waldmann by very elementary matrix interpretations found as a result of extensive computer search. In this talk we presentaa -> bc bb -> ac cc -> ab
| Jürgen Giesl: Disproving Termination of Term Rewriting
Most existing techniques for automated termination analysis
try to prove termination and there are hardly any methods to prove
non-termination. In this work, we introduce techniques to disprove termination
of term rewrite systems (TRSs) within the so-called dependency pair
framework. Apart from disproving full termination, we also present new methods which can
disprove termination under the innermost evaluation strategy (i.e., they can
disprove innermost termination). Innermost termination is particularly
important in practice, since it corresponds to termination under the eager
call-by-value evaluation strategy used in many programming languages.
We implemented and evaluated our contributions in the automated termination prover AProVE. Due to these results, AProVE was the winning tool in the International Competition of Termination Provers 2005, both for proving and for disproving (innermost) termination of term rewriting.
The talk is based on joint work with Rene Thiemann and Peter Schneider-Kamp.