Rewriting theory is the study of relations and, in particular,
relations on symbolic expressions (terms). Relations can for instance
be used to model transition systems, operational semantics,
computation rules, and decide equational theories.

Term rewriting is based on the notion of pattern
matching. Programming languages like OCaml and Haskell, or proof
assistants like Agda or Coq use a restricted form of pattern
matching. Programming languages like Maude and proof assistants like
Dedukti allow a more general form of pattern-matching.

Two properties will be of particular interest for us: termination
(there is no infinite sequence of rewrite steps) and confluence (the
order of rewrite steps does not matter).

This course aims at introducing the fundamentals of rewriting
theory, and in particular term rewriting systems, and some basic
termination and confluence results and techniques used in nowadays
state-of-the-art termination and confluence automated provers.

21 December: non-modularity of termination, incremental termination proofs, well-quasi-orders, [Lecture 6][Exercises 6][Solutions 6]deadline to return homework

11 January: introduction to deduction modulo rewriting by invited speakerGilles Dowek, and demonstration of termination and confluence tools [Exercises 7][Solutions 7]