TeReSe
17th Informal Workshop on Term Rewriting March 28, 2012 Aachen, Germany Important Dates  Practical Information  Preliminary Schedule  Abstracts 
Participant registration  Sunday, March 25 
If you are interested in giving a talk or if you have any other questions regarding the organization of the meeting, please contact:
Thomas Ströder
stroeder@informatik.rwthaachen.de
Wednesday, March 28 

13:30    14:00  Soundness and Completeness of Infinitary Term Graph Rewriting  
Patrick Bahr, Københavns Universitet  
14:00    14:30  CRSX: a polymorphic specification language (Or: what I did last summer)  
Cynthia Kop, Vrije Universiteit Amsterdam  
14:30    15:00  Polynomial Interpretations for HigherOrder Rewriting  
Carsten Fuhs, University College London  
15:00    15:30  Coffee Break  
15:30    16:00  Expressibility in the Lambda Calculus with Letrec  
Jan Rochel, Universiteit Utrecht  
16:00    16:30  CARPA: Counter examples in Abstract Rewriting Produced Automatically  
Hans Zantema, TU Eindhoven / RU Nijmegen  
16:30    17:00  Detecting NonLooping NonTermination  
Jürgen Giesl, RWTH Aachen 

17:00    17:30  TeReSe business meeting  
18:00    ??:??  Dinner at Waldschenke (Lütticher Str. 340)  location info  
Patrick Bahr: Soundness and Completeness of Infinitary Term Graph Rewriting 
Infinitary term rewriting provides a tool for reasoning about infinite
computations and infinite data as we conceptually find them in lazy
functional programs. Term graph rewriting, on the other hand, captures
the other defining aspect of lazy functional programming:
sharing. With the goal of unifying both paradigms, we generalise the
infinitary term rewriting theory to term graphs. We follow two
approaches known from infinitary term rewriting: one based on a metric
and another based on a partial order on term graphs.

Cynthia Kop: CRSX: a polymorphic specification language (Or: what I did last summer) 
The CRSX system, a functional programming language particularly designed to specify compilers, can be seen as a formalism of higherorder term rewriting. I will discuss this formalism, its peculiarities, and its relation to other higherorder term rewriting formalisms. 
Carsten Fuhs: Polynomial Interpretations for HigherOrder Rewriting 
The termination method of weakly monotonic algebras, which has been
defined for higherorder rewriting in the HRS formalism, offers a lot
of power, but has seen little use in recent years. We adapt and extend
this method to the alternative formalism of algebraic functional
systems, where the simplytyped λcalculus is combined with
algebraic reduction. Using this theory, we define higherorder
polynomial interpretations, and show how the implementation
challenges of this technique can be tackled. A full implementation is
provided in the termination tool
WANDA.

Jan Rochel: Expressibility in the Lambda Calculus with Letrec 
We investigate the relationship between finite terms in lambdaletrec,
the lambda calculus with `letrec', and the infinite lambda terms they
express. As there are easy examples of infinite lambda terms that,
intuitively, are not unfoldings of terms in lambdaletrec, we consider
the question: How can those infinite lambda terms be characterised
that are lambdaletrecexpressible in the sense that they can be
obtained as infinite unfoldings of terms in lambdaletrec?

Hans Zantema: CARPA: Counter examples in Abstract Rewriting Produced Automatically 
Rewriting notions like termination, normal forms, and confluence can be described in an abstract way referring to rewriting only by a binary relation. Several theorems on rewriting, like Newman's lemma, can be proved in this abstract setting. For investigating possible generalizations of such theorems, it is fruitful to have counter examples showing that particular generalizations do not hold. In this talk a technique is presented to find such counter examples fully automatically by the tool CARPA.

Jürgen Giesl: Detecting NonLooping NonTermination 
We introduce a technique to prove nontermination of term rewrite systems automatically. In contrast to most previous approaches, our technique is also able to detect nonlooping nontermination. 