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, 2: abstract rewriting: definition and properties of ARSs (Jörg Endrullis)
- 3: term rewriting systems: a formal introduction to term rewriting (Femke van Raamsdonk) and a look into variations of TRSs (Cynthia Kop)
- 4: exercises
- 5: monotonic algebras (termination): an introduction to polynomial interpretations and the more general monotonic algebras
- 6: the recursive path ordering (termination: an introduction of the lexicographic and recursive path ordering, and their extraordinary soundness proof (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 and many informal examples (Femke van Raamsdonk)
- 12: exercises (Femke van Raamsdonk)
- 13: the dependency pair framework (termination): an explanation of the dependency pair framework and how it can be used to prove termination (Cynthia Kop)
- 14: exercises (Cynthia Kop)
- 15: orthogonality (confluence): a simple yet powerful method to prove confluence in many practical cases, along with exercises (Jörg Endrullis)
- 16: decreasing diagrams (confluence): a more advanced technique to prove confluence (Jörg Endrullis)
- 17: recap, and a short introduction to advanced topics in active research (including complexity and various topics discussed on the whiteboard).