Programming with dependent types and rewrite rules (Delivered in English)
- LecturerProf. Jean-Pierre Jouannaud (Université Paris-Saclay, Ecole Normale Supérieure de Paris-Saclay, INRIA)
Host: Bow-Yaw Wang - Time2024-11-04 (Mon.) 10:30 ~ 12:30
- LocationAuditorium 106 at IIS new Building
Abstract
Dedukti is a logical framework based on dependent type theory and higher-order rewrite rules including the beta rule. The goal is to use Dedukti as an exchange proof format, by encoding various logics of interest in Dedukti. Proofs in a given logic, say HOL become then checkable in Dedukti, enhancing confidence in their correctness.
They can also by transfered from one system to another via Dedukti. So far, we can import the whole HOL and HOL-Light libraries, the Matita library, parts of Coq and Agda libraries (both are moving targets due to the management of universes), and export to some of these systems, essentially HOL.
Defining these encodings is a kind of programming activity in the Dedukti language, making a heavy use of rewrite rules, which need to satisfy three properties: type preservation, termination and confluence (apart from faithfullness of the encoding).
In this talk, I will concentrate on confluence:
- explain the theoretical difficulties,
- give examples of confluent and non-confluent encodings,
- explain the theoretical tools on which confluence proofs are based,
- picture the rapidly moving state of the art.
They can also by transfered from one system to another via Dedukti. So far, we can import the whole HOL and HOL-Light libraries, the Matita library, parts of Coq and Agda libraries (both are moving targets due to the management of universes), and export to some of these systems, essentially HOL.
Defining these encodings is a kind of programming activity in the Dedukti language, making a heavy use of rewrite rules, which need to satisfy three properties: type preservation, termination and confluence (apart from faithfullness of the encoding).
In this talk, I will concentrate on confluence:
- explain the theoretical difficulties,
- give examples of confluent and non-confluent encodings,
- explain the theoretical tools on which confluence proofs are based,
- picture the rapidly moving state of the art.