ISR 2026 — 15th International School on Rewriting
Basic track
The course provides a comprehensive introduction to term rewriting. Term rewriting is a general model of computation which has been successfully applied in many areas of computer science. Here one can think of the analysis and implementation of algebraic specifications of abstract data types, the foundations of functional (logic) programming, automated theorem proving, and code optimization in compilers, to name just a few.
Topics to be discussed will include (but are not limited to): abstract rewriting systems, term rewriting systems, equational reasoning, termination, confluence, completion, Newman's lemma, critical pairs, monotonic algebras, path ordering, and dependency pairs.
The course consists of 17 slots of 90 minutes (divided into both lectures and exercise sessions), plus one optional 90-minute slot for the final test (for students requiring an ECTS certificate).
Lecturers
Track schedule (see the program for the overall program outline)
| Sunday | Monday | Tuesday | Wednesday | Thursday | |
|---|---|---|---|---|---|
| 9:00–10:30 | 1 | 5 | 9 | 11 | 15 |
| 10:30–11:00 | break | ||||
| 11:00–12:30 | 2 | 6 | 10 | 12 | 16 |
| 12:30–13:30 | break | ex cur sion |
break | ||
| 13:30–15:00 | 3 | 7 | 13 | test | |
| 15:00–15:30 | break | break | |||
| 15:30–17:00 | 4 | 8 | 14 | 17 | |
| 17:00–18:00 | dinner | dinner | |||
Topics (tentative)
- 1: abstract rewriting systems: definition and properties (Jörg Endrullis)
- 2: term rewriting systems, lambda calculus and exercises (Femke van Raamsdonk, Jörg Endrullis)
- 3: termination: polynomial interpretations (Femke van Raamsdonk, Cynthia Kop)
- 4: exercises
- 5: termination: monotonic algebras (including exercises) (Cynthia Kop)
- 6: termination: the recursive path ordering (including exercises) (Jörg Endrullis)
- 7: confluence: unification and critical pairs (Femke van Raamsdonk)
- 8: exercises
- 9, 10: weak and strong normalization for typed lambda calculus
- 11: equational reasoning and completion (Femke van Raamsdonk)
- 12: exercises (Femke van Raamsdonk)
- 13: termination: the dependency pair framework (Cynthia Kop)
- 14: exercises
- 15: confluence: decreasing diagrams (including exercises) (Jörg Endrullis)
- 16: confluence: orthogonality (including exercises) (Jörg Endrullis)
- 17: an overview of advanced topics in active research