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.
PVS is a proof assistant based on higher-order logic featuring implicit predicate subtyping, that is, users can define types by restricting some super-type with arbitrary predicates (e.g. the type of prime numbers). PVS is for instance used by NASA to prove the correctness of algorithms in aeronautics.
In [8], Frédéric Gilbert described and studied the core aspects of PVS by defining two systems: PVS-Core featuring implicit predicate subtyping and PVS-Cert featuring explicit predicate subtyping. Then, in [9,10], Gabriel Hondet showed how to represent PVS-Cert in Dedukti and developed a tool, Personoj, for translating PVS terms and propositions into Dedukti.
Objective: The goal of this project is to extend Personoj so as to translate not only the terms and propositions of PVS but also its proofs. PVS proofs are "big-step" proofs. A "big-step" proof is a sequence of propositions starting from the assumptions and ending into the proved proposition, where one indicates from which previous intermediate propositions each proposition is obtained without giving much details on how it is obtained. But Dedukti expects detailed "small-step" proofs. Therefore, to translate PVS proofs into Dedukti, it is necessary to turn a "big-step" proof into a "small-step" proof.
Workplan: One will start by getting some familiarity with the various tools involved in this project, as well as the λΠ-calculus modulo rewriting and how to represent proofs in this setting. To try to reconstruct a small-step proof from a big-step one, one can try to adapt Ekstrakto which uses automated theorem provers generating Dedukti proofs to check each big step [11].
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] Extending higher-order logic with predicate subtyping: application to PVS, Frédéric Gilbert, PhD thesis, Université Sorbonne Paris Cité, 2018.
[9] Expressing predicate subtyping in computational logical frameworks, Gabriel Hondet, PhD thesis, Université Paris-Saclay, 2022.
[10] Encoding of Predicate Subtyping with Proof Irrelevance in the λΠ-calculus Modulo Theory, Frédéric Blanqui and Gabriel Hondet, TYPES'20 post proceedings, LIPIcs 188, 2021.
[11] Integrating Automated Theorem Provers in Proof Assistants, Yacine El Haddad, PhD thesis, Université Paris-Saclay, 2021.