Internship subject: Translating Lean to Dedukti

Level: M1-M2

Supervisor: Frédéric Blanqui and Floris van Doorn

Place: Deducteam, Laboratoire Méthodes Formelles (LMF), ENS Paris-Saclay, 4 avenue des Sciences, Gif-sur-Yvette, and Mathematics Department, University Paris-Saclay, bâtiment 307, rue Michel Magat, Orsay (there are 2.7 km between the two places)

Context: This internship 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 because it can only be partial. Indeed, proof systems sometimes have incompatible features: combining them can make them inconsistent. Therefore, to translate a proof from one system to the other, we first 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 are a number of tools for transforming those proofs and translate them back to various other systems: HOL-Light, Coq, PVS, Lean, etc. [7].

Lean4[8] is a dependently typed proof assistant and programming language. It has an expressive logic with inductive types and universes, similar to Coq. It has a powerful elaborator, tactic language, macro expansion system [9] and compiler. It's predecessor Lean3 has a large mathematical library mathlib, that will be ported to Lean4 in 2022, and is of great interest for other proof systems.

Finally, note that there exist several type-checkers for Dedukti files: dkcheck, kontroli and lambdapi. Lambdapi is also an interactive proof assistant (it extends Dedukti with many features like implicit arguments, proof tactics, etc.).

Objective: The goal of this internship is to develop in Lean4 a translator from Lean4 to Dedukti. Compared to the encodings already done for Coq or Agda, a possible difficulty is the handling of proof irrelevance, which is a specific feature of Lean meaning that any two proofs of the same proposition are identified [10].

Workplan: The intern will start by getting some familiarity with the λΠ-calculus modulo rewriting and the Dedukti or Lambdapi languages, the meta-theory of Lean [10], and the encodings of Coq and Agda in Dedukti [3,6]. Concerning proof irrelevance, the intern could perhaps get some inspiration from the encoding of a particular case of proof irrelevance in [4].

Requirements: Some familiarity with Lean.

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] The Lean 4 Theorem Prover and Programming Language, Leonardo de Moura and Sebastian Ullrich, CADE'21.

[9] Beyond Notations: Hygienic Macro Expansion for Theorem Proving Languages, Sebastian Ullrich and Leonardo de Moura, IJCAR'20.

[10] The type theory of Lean, Mario Carneiro, 2019.


Statcounter W3C Validator Last updated on 27 June 2022. Come back to main page.