Friday afternoon 9 December 2011

This TeReSe, an afternoon with presentations on rewriting, took place on Friday December 9th 2011 at

Drift 21, Room 0.03, Utrecht
(the same building ISR 2010 took place in
coordinates: +52 degrees 5 minutes 39.7032 seconds, +5 degrees 7 minutes 24.6108 seconds, i.e. 52.094362,5.123503)

TeReSes take place at locations with an active rewriting community, in or close to the Netherlands (Aachen, Amsterdam, Eindhoven, Nijmegen, Utrecht).

We were happy to receive so many of you.
Clemens Grabmayer and Vincent van Oostrom


title of talk
13.30 Jan Willem Klop
(VU Amsterdam)
Zip-specifications and automatic sequences
14.15 Carsten Fuhs
(RWTH Aachen)
Harnessing first order termination provers using higher order dependency pairs
15:00 break
15.30 Hans Zantema
(TU/e and Radboud University)
Type preservation in simply typed lambda calculus by abstract reduction techniques
16.15 Vincent van Oostrom
(Utrecht University)
A well-founded partial order on the free involutive monoid
17.00 business meeting
17.30 end

After the meeting we had a joint dinner in Vietnamese restaurant Saigon (within walking distance of the venue)

The next TeReSe will be organized by the group of Jürgen Giesl, in Aachen in the spring of 2012.
Hope to see you all there.


Zip-specifications and automatic sequences:
Streams and zip-specifications
Unique solvability versus productivity
Observation graphs
Comparing zip-specifications
Finite observation graphs
Generalisations: zip-k-specifications
Equality of zip-k-specifications is decidable.
How far can we go?
joint work with Jörg Endrullis (VU Amsterdam), Clemens Grabmayer (Utrecht University), Dimitri Hendriks (VU Amsterdam), and Larry Moss (Indiana University)

Harnessing first order termination provers using higher order dependency pairs:
Many functional programs and higher order term rewrite systems contain, besides higher order rules, also a significant first order part. We discuss how an automatic termination prover can split a rewrite system into a first order and a higher order part. The results are applicable to all common styles of higher order rewriting with simple types, although some dependency pair approach is needed to use them.
joint work with Cynthia Kop (VU Amsterdam)

Type preservation in simply typed lambda calculus by abstract reduction techniques:
Usually, in simply typed lambda calculus the syntax of types is separate from the syntax of lambda expressions. In this talk we combine these two. In this extended syntax we have two kinds of computations: abstract steps for computing the type of a lambda expression, and concrete steps for doing beta-reductions. We focus on call-by-value steps, and analyze how the separate steps may commute. One consequence of these investigations is that types are preserved by concrete steps. Another consequence is that restricting to well-typed expressions, the union of abstract and concrete steps is confluent. For the latter we apply a theorem for concluding confluence by abstract properties. For showing that all conditions of this theorem are essential, we give counterexamples that are found by SAT solving techniques.
joint work with Aaron Stump, Garrin Kimmell and Ruba El Haj Omar (University of Iowa), based on their RTA 2011 paper (best paper award)

A well-founded partial order on the free involutive monoid:
We lift the construction of the free involutive monoid from sets to well-founded partial orders. This is then applied to proving confluence.