MPRI, 24 hours, 3 credits [serveur pédagogique]
Schedule: Thursday 8:30-12:45, from 17 September 2020 to 12 November 2020
Place: ENS Paris-Saclay, room 2E29
Staff: Frédéric Blanqui (lectures, 8:30-10:30) and Gabriel Hondet (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.
To go further, have a look at the 11th International School on Rewriting (ISR 2019)!
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 2020-2021)