**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.

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