Curriculum M1 MPRI at ENS Paris-Saclay

PROT: Proof Theory

Description: In a mathematical proof, one can distinguish between steps of reasoning and steps of calculation. This course aims to provide a general framework for expressing these two aspects and to introduce the basic tools needed to verify key properties of the calculation rules employed (such as termination, confluence, and models). It also provides an introduction to dependent types and how they can be used to represent formulas and proofs from various logics in a modular way.

Outline:

  1. Using rewriting to decide equality in an equational theory (Knuth-Bendix completion). Basic techniques for demonstrating the confluence of a set of rewrite rules (critical pairs, orthogonal systems).
  2. Rewriting theory; basic techniques for demonstrating the termination of a set of rewrite rules (dependency pairs, recursive path ordering, polynomial interpretations).
  3. Distinguishing reasoning from computation: natural deduction modulo an equational theory. Models of a theory with rewrite rules.
  4. Examples of purely computational theories—i.e., without axioms: arithmetic, set theory, simple type theory.
  5. Cut elimination and constructivity in natural deduction modulo a theory.
  6. Introduction to dependent types and Pure Type Systems.
  7. Modular representation of formulas and proofs from various logics in the λΠ-calculus modulo rewriting—ranging from first-order logic to higher-order logic or the Calculus of Constructions, which forms the basis of modern proof assistants.


References: