ISR 2024 – Track C
Termination and Complexity in Higher-Order Term Rewriting
Lecturer
Cynthia Kop Radboud University Nijmegen
Course Description
In this course, we will dive into (simply-typed) higher-order term rewriting systems. What makes them different from first-order rewriting, what makes them similar, and how can typical analysis methods for rewriting — in particular, techniques for termination and complexity analysis — be extended to them?
Content
-
day 1: motivations, definitions, challenges
handout part a (foldable) slides (part a)
handout part b (foldable) slides (part b) -
day 2: computability, higher-order recursive path ordering
handout (foldable) slides -
day 3: static dependency pairs
handout (foldable) slides -
day 4: monotonic algebras as a method for termination and complexity
handout (foldable) slides
Course Link
link