**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 [1,2] is a powerful logical
framework allowing users to define their own logic and represent
proofs in those user-defined logics. A proof checker for this
calculus is implemented in Dedukti [3] and Lambdapi [4], aka Dedukti
v3, an interactive extension of Dedukti. Hence, in Dedukti, one can
represent first-order logic and its proofs, simple type theory and
its proofs, the Agda [5] logic and its proofs, etc.
Guillaume Genestier, a PhD student of mine who recently finished his
PhD, found out an encoding of Agda logic in Dedukti [6], and started
to develop a translator from Agda to Dedukti [7] using this
encoding. This tool can currently translate about 25% of the Agda
standard library.

**Objectives:** Increase the number of Agda files that
can be translated to Dedukti. There are many features of Agda that
still need to be translated, in particular coinductive
definitions [8]. The encoding of coinductive definitions in the
λΠ-calculus modulo rewriting has never been studied yet. This would
be useful not only for Agda but for any system allowing coinductive
definitions (Coq for instance).

**Workplan:** The intern will start by getting some
familiarity with the λΠ-calculus modulo rewriting, Lambdapi, Agda, the
code base of Agda, and agda2dk. The intern will then work on the
encoding of coinductive definitions in the λΠ-calculus modulo
rewriting, and implement it in agda2dk.

**Requirements:** Some familiarity with Haskell.

**References:**

[1] A. Assaf, G. Burel, R. Cauderlier, D. Delahaye, G. Dowek, C. Dubois, F. Gilbert, P. Halmagrand, O. Hermant, and R. Saillard. Dedukti: a logical framework based on the λΠ-calculus modulo theory, 2016. Draft.

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

[3] Dedukti

[4] Lambdapi

[6] G. Genestier, Encoding Agda Programs using Rewriting, FSCD'20.

[7] Agda2Dedukti

[8] A. Abel, B. Pientka, A. Setzer, and D. Thibodeau, Copatterns: Programming Infinite Structures by Observations, Proceedings of the 40th ACM Symposium on Principles of Programming Languages (POPL), 2013.

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