MPRI, 24 hours, 3 credits (1 homework + 1 exam) [serveur pédagogique]
Schedule: Thursday 8:30-12:45, from 16 November 2017 to 18 January 2018.
Place: ENS Cachan, Cournot building, room 321
Staff: Frédéric Blanqui (lectures, 8:30-10:30) and Alessio Mansutti (exercises, 10:45-12:45)
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.
Correction of the homework
Correction of the exam
Online termination, confluence or completion tools:
More tools are available on:
Related lectures: Well quasi-orders for algorithms, Gilles Dowek's lecture on proofs in theories (every two years, next in 2018-2019)