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 formats/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.
Using SMT solvers in proof assistants is very useful as they can automatically discharge many proof obligations involving common theories like linear arithmetic, bit-vectors, etc. But SMT solvers are complex and optimized software subject to bugs. In order to check the output of SMT solvers, some proof formats have been developed, like Alethe [8,9] which is output by the SMT solver veriT (an Alethe output for cvc5 is also under development). However, the proofs in these formats are usually big-step proofs as opposed to the small-steps proofs that are implemented in proof assistants and, in particular, in Dedukti and Lambdapi. Therefore, to use an SMT solver in a proof assistant, it is necessary to generate small-step proofs from those big-step proofs. [10] describes such a translation from Alethe to Isabelle. However, Isabelle is based on simple type theory with the axiom of choice while Dedukti and Lambdapi are based on dependent type theory modulo rewriting.
Objective: The goal of this project is to develop a tool for generating small-step proofs in Dedukti or Lambdapi from big-step proofs in the Alethe proof format. One potential difficulty is the handling of Hilbert's choice operator ε for representing Skolem symbols. Another one is the handling of implicit rules.
Workplan: One will start by getting some familiarity with the λΠ-calculus modulo rewriting and the Dedukti or Lambdapi languages, the encoding of first-order logic in Dedukti or Lambdapi [1,2], and the Alethe proof format itself [8,9]. Then, one can reuse some code from [10] (parser for Alethe), and adapt it to Dedukti or Lambdapi.
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] Alethe: Towards a Generic SMT Proof Format, Hans-Jörg Schurr, Mathias Fleury, Haniel Barbosa and Pascal Fontaine, PxTP'21.
[9] Stronger SMT Solvers for Proof Assistants, Hans-Jörg Schurr, Université de Loraine, 2022.
[10] Reliable Reconstruction of Fine-Grained Proofs in a Proof Assistant, Hans-Jörg Schurr, Mathias Fleury and Martin Desharnais, CADE'21. [code]