ISR 2024 – Track C

Applications of Rewriting Theory in Proof Systems Interoperability

Lecturer

Frédéric Blanqui   Inria

Course Description

In this course, we are going to see how rewriting can be useful to represent proofs, so as to facilitate their exchange between provers. In practical sessions, we will learn how to use the interactive logical framework Lambdapi to define functions and types using rewriting, and represent the proofs of some proof systems. We will also see how to try to automatically check some important properties of the rewrite systems one can define in Lambdapi.

Outline

1. Introduction to proof systems: interoperability; introduction to the λΠ-calculus modulo rewriting (λΠ/R) (part 1): λ-calculus, dependent types
      slides (part a, part b, part c)

To prepare the practical session tomorrow, install Opam and Lambdapi on your machine.

2. Introduction to λΠ/R (part 2): pure type systems, rewriting; introduction to the Lambdapi proof assistant, practical session on Lambdapi


3. Encoding logics in λΠ/R: first-order logic, polymorphism, higher-order logic, pure type systems, …


4. Properties of λΠ/R: decidability of type-checking, subject-reduction, confluence, termination, dependencies between these properties