ISR 2024 – Track C

Interoperability of Proof Systems using Lambdapi

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.

1. Introduction to proof system interoperability and Lambdapi. How to represent the proofs of first-order logic in Lambdapi? Exercises in Lambdapi.


2. How to represent the proofs of higher-order logic in Lambdapi? What if we add predicate subtyping like in PVS? To be or not to be non left-linear? How to check that a rewrite rule preserves typing? Knuth-Bendix to the rescue.


3. Can we encode more complex type systems in Lambdapi? The case of Agda, Coq or Lean type universes: associativity and commutativity to the rescue.


4. How to check that a set of rewrite rules terminate in Lambdapi? Dependency pairs and reducibility candidates to the rescue. Proof system interoperability today. What are the tools? What can be done?