## Higher-order term rewritingCynthia Kop (Radboud University) |

Some material will be available here.

In this lecture, I will discuss *higher-order* term rewriting, a way to combine the benefits of term rewriting and the lambda calculus. I will present some of the considerations (such as typing, polymorphism and matching), some applications, and show how the basic analysis techniques for confluence and termination extend from first-order to higher-order term rewriting systems.

**Outline of the lecture**

The lecture will focus on (untyped) CRSs, but explain why typing is useful later. I will discuss a simple version of the higher-order recursive path order for termination, and orthogonality for confluence. Each of the different topics will be interleaved with exercises.

**Exercises or experiments**

Absolutely!

**Bibliographical references**

- Terese.
*Term Rewriting Systems*, volume 55 of Cambridge Tracts in Theoretical Computer Science. Cambridge University Press, 2003. - J.W. Klop, V. van Oostrom, and F. van Raamsdonk.
*Combinatory reduction systems: introduction and survey*. Theoretical Computer Science, 121(1-2):279–308, 1993. - J. Jouannaud and A. Rubio.
*The higher-order recursive path ordering*. In*Proceedings of the 14th Annual Symposium on Logic in Computer Science*(LICS ’99), IEEE, pages 402–411, 1999. - (perhaps) J.C. van de Pol.
*Termination of Higher-order Rewrite Systems*. PhD thesis, University of Utrecht, 1996.