Supervisor: Frédéric Blanqui
Place: Deducteam, Laboratoire Méthodes Formelles (LMF), ENS Paris-Saclay, 4 avenue des Sciences, Gif-sur-Yvette
Context: This project is about formal proofs as digital objects, more specifically the translation of formal proofs between different proof systems. Formal proofs are used in mathematics but also in the industry for certifying the correctness of protocols, software and hardware.
Interoperability is a very important feature in computer science and engineering to avoid useless work duplication and allow more safety. Unfortunately, interoperability between proof systems is not well developed. One important difficulty is that proof systems may have incompatible features: their combination may be inconsistent. Therefore, to translate a proof from one system to the other, we need to analyze the features of the first system used in the proof and check whether they are compatible with the features of the target system.
The λΠ-calculus modulo rewriting, and its implementation Dedukti, is a powerful logical framework allowing users to define their own logic and represent the proofs in those logics [1,2]. For instance, one can represent in Dedukti first-order logic and its proofs, simple type theory and its proofs, the Isabelle logic and its proofs [5], the Coq logic and its proofs [3], the Agda logic and its proofs [6], etc. In addition, there is a number of tools for transforming those proofs and translate them back to various other systems: HOL-Light, Coq, PVS, Lean, etc. [7].
There exist several tools for checking the correctness of Dedukti files: dkcheck, kontroli and lambdapi. While dkcheck and kontroli are mere checkers taking complete Dedukti files as input, Lambdapi is a proof assistant featuring implicit arguments, type inference, coercions, tactics, the possibility of calling external automated theorem provers, etc. for building Dedukti proofs interactively.
Objective: Many proofs are about recursively defined functions or use recursively defined functions. Therefore translating proofs from one system to the other requires to translate recursively defined functions. There are many ways to represent recursive function definitions: with a general fixpoint operator (PVS), possibly with match/case constructions (Coq); with recursors like within Gödel's system T; with pattern-matching clauses (OCaml, Agda); with rewrite rules. See for instance [13] for some partial survey. There has already been a number of propositions for translating some of these representations to Dedukti [8,9,10,3]. The first goal of this project is to make a detailed review of all these representations and all the proposed encodings in Dedukti, compare them, describe the advantages and disadvantages of each one. The second goal is to look for known algorithms [11,12] or propose new ones for translating recursive definitions from one representation to the other. For implementations, see for instance Equations in Coq, and some work in progress in Agda.
References:
[1] Dedukti: a logical framework based on the λΠ-calculus modulo theory, A. Assaf, G. Burel, R. Cauderlier, D. Delahaye, G. Dowek, C. Dubois, F. Gilbert, P. Halmagrand, O. Hermant, and R. Saillard, Draft, 2016.
[2] Some axioms for mathematics, F. Blanqui, G. Dowek, E. Grienenberger, G. Hondet and F. Thiré, FSCD 2021.
[3] Higher-Order Confluence and Universe Embedding in the Logical Framework, Gaspard Férey, PhD, 2021.
[4] Encoding of Predicate Subtyping with Proof Irrelevance in the λΠ-Calculus Modulo Theory, Gabriel Hondet and Frédéric Blanqui, TYPES'20.
[5] Translating proofs between Isabelle and Dedukti, Yann Leray, M1 Internship Report, 2021.
[6] Encoding Agda Programs Using Rewriting, G. Genestier, FSCD'20.
[7] Sharing a Library between Proof Assistants: Reaching out to the HOL Family, François Thiré, LFMTP'18.
[8] A framework for defining computational higher-order logics, A. Assaf, PhD thesis, Ecole Polytechnique, 2015.
[9] Object-Oriented Mechanisms for Interoperability between Proof Systems, Raphaël Cauderlier, PhD thesis, CNAM, 2016.
[10] Interoperability between proof systems using the logical framework Dedukti, François Thiré, PhD thesis, Université Paris-Saclay, 2020.
[11] Dependent pattern matching and proof-relevant unification, Jesper Cockx, PhD thesis, KU Leuven, 2017.
[12] Equations Reloaded: High-Level Dependently-Typed Programming and Proving in Coq, Matthieu Sozeau and Cyprien Mangin, ICFP'19.
[13] Partiality and Recursion in Interactive Theorem Provers — An Overview, Ana Bove, Alexander Krauss and Matthieu Sozeau, MSCS, 2016.