Internship subject: Encoding Agda and coinduction in 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 [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

[5] Agda's documentation

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


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