Programming with dependent types and rewrite rules (以英文演講)
- 講者Jean-Pierre Jouannaud 教授 (Université Paris-Saclay, Ecole Normale Supérieure de Paris-Saclay, INRIA)
邀請人：王柏堯 - 時間2024-11-04 (Mon.) 10:30 ~ 12:30
- 地點資訊所新館106演講廳
摘要
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.