MPRI, 24 hours, 3 credits [serveur pédagogique]
Schedule: Thursday 8:30-12:45 from September to October 2024 (TBC)
Place: ENS Paris-Saclay, room 1E14 (TBC)
Staff: Frédéric Blanqui (lectures, 8:30-10:30) and Théo Vignon (TBC, 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 Lambdapi 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.
Planning:
To go further, have a look at the International School on Rewriting.
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 2022-2023)