3rd International School on Rewriting

21 – 26 July 2008, Obergurgl, Austria

Program – Track A – Introduction to Term Rewriting

Lecturers

Pierre Lescanne
Femke van Raamsdonk

Introduction

The goal of this course is to provide an introduction to term rewriting on the master/PhD level. No background knowledge is assumed. A tentative schedule of the lectures is as follows:

• introduction (motivation, equational reasoning, simplification),
• mathematical background (relations, well-founded induction),
• abstract rewriting (basic notions, interrelations, Newman’s lemma),
• term rewriting (terms, unification and matching, reduction, combinatory logic),
• lambda calculus (lambda-terms, beta-reduction, expressiveness),
• termination (dependency pairs, recursive path order, monotone algebras, semantic labeling),
• confluence (critical pairs, critical pair lemma, orthogonality, developments),
• strategies (normalization, sequential strategies, perpetual strategies).

Material

• Pierre Lescanne
  • lecture notes
  • slides
• Femke van Raamsdonk
  • slides
• exercises
  • exercises (part 1)
  • exercises (part 2)
  • exercises (part 3)
  • exercises (part 4)
  • exercises (all)