ISR 2024 – Track A

Term Rewriting

This site provides supporting material for Track A of ISR 2024.

Lecturer

Aart Middeldorp

University of Innsbruck

Content

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.

The following topics will be discussed: examples, terms, matching algorithm, abstract rewrite systems, Newman's lemma, multiset orders, equational reasoning, algebras, term rewrite systems, undecidability, congruence closure, termination, polynomial interpretations, LPO, unification, critical pairs, completion, first-order theory of rewriting, KBO, normalization equivalence, abstract completion, confluence, orthogonality, strategies, normalization, strategy annotations, simple termination, proof terms, dependency pairs, Z property.

The course consists of 20 slots of 90 minutes: 13 lecture slots, 6 exercises sessions, and a final test (for students requiring an ECTS certificate).