MPRI, 24 hours, 3 credits (1 homework + 1 exam)
Schedule: Friday 14:00-18:15, from 18 November 2016 to 13 January 2017.
Place: ENS Cachan, Cournot building, room 205
Staff: Frédéric Blanqui (lecture, 14:00-16:00) and Jérémy Dubut (exercises, 16:15-18:15)
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.
Online termination, confluence or completion tools:
More tools are available on: