Internship subject: Translating Isabelle proofs to Dedukti

Level: M1-M2

Supervisor: Frédéric Blanqui

Place: Deducteam, Laboratoire Méthodes Formelles (LMF), ENS Paris-Saclay, 4 avenue des Sciences, Gif-sur-Yvette, France.

Context: This internship is about formal proofs, more specifically their translation between different proof systems.
Formal proofs are used in mathematics but also in the industry for certifyingthe correctness of protocols, software and hardware.
Interoperability is a very important feature in computer science and engineering to avoid useless work duplication and 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 make them inconsistent. Therefore, to translate a proof from one system to another one, we first need to analyze the features of the first system used in the proof and check whether they are compatible with the features ofthe target system.
The λΠ-calculus modulo rewriting is a powerful logical framework allowing users to define their own logic and represent proofs in those user-defined logics [1,2,5]. A proof checker for this calculus is implemented in Dedukti and Lambdapi, an interactive extension of Dedukti. Hence, in Dedukti, one can represent first-order logic and its proofs, simple type theory and its proofs, etc.
Isabelle [3,4] is one of the most used proof assistants in the world. It is based on simple type theory and features type classes. Makarius Wenzel, the main developer of Isabelle, started to develop a translation of Isabelle proofs to Dedukti in https://github.com/Deducteam/isabelle_dedukti.

Objectives: Write down a description of the translation and prove its correctness, and investigate why Isabelle gets problems for exporting its proofs (sharing/modularity problem?).

Workplan: The intern will start by getting some familiarity with the λΠ-calculus modulo rewriting, Lambdapi, simple type theory, Isabelle, and the translator from Isabelle to Dedukti. She/he will write down a description of Isabelle terms, their encoding in the λΠ-calculus modulo rewriting, and prove its correctness. She/he will then study how Isabelle exports its proofs and why it does not scale up in some cases.

Requirements: Some familiarity with a functional programming language (Isabelle is written in ML and Scala).

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, 2016. Draft.

[2] Some axioms for mathematics, F. Blanqui, G. Dowek, E. Grienenberger, G. Hondet and F. Thiré, FSCD 2021.

[3] The Isabelle/Isar Implementation, M. Wenzel, 2021.

[4] Isabelle: a generic theorem prover, L. Paulson, LNCS 828, 1994.

[5] A framework for defining logics, R. Harper and F. Honsell and G. Plotkin, JACM 40(1), 1993.


Statcounter W3C Validator Last updated on 13 October 2021. Come back to main page.