Internship subject: Structured proofs in Lambdapi


Level: L3-M1

Supervisor: Frédéric Blanqui

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

Context: Dedukti v3 aka Lambdapi is a proof assistant, that is, a tool allowing to build and check mathematical proofs formally. Dedukti is also a logical framework, that is, it does not come with a pre-defined logic: the user has to define it, which is usually easy [1]. Yet, it provides basic proof tactics that can be used in various user-defined logics. However, there is currently nothing to structure proofs which makes their reading and maintenance difficult and fragile.

Objectives: The objective of this internship is to design and implement in OCaml a language for structuring proof scripts in Lambdapi. Proofs inherently have a tree structure. For instance, to prove that a property P(n) holds for all natural numbers n, one can proceed by induction on n. To this end, one first needs to prove P(0) and also that ∀n,P(n)⇒P(n+1), which makes two new subgoals, and the proof of each subgoal may need the application of further proof tactics. It is therefore important to know, among the following tactics given by the user, what are those corresponding to the first subgoal and those corresponding to the second subgoal.

Workplan: If the intern is not familiar with the use of proof assistants, he will start by getting some familiarity with current proof assistants (Coq and Lambdapi) by reading some textbooks and manuals, and making simple proofs [3]. The intern will then read a few articles describing various approaches to proof languages [4,5,2], and compare them. Based on this study, the intern will propose a proof language for Lambdapi. After validation, the intern will implement it, and do some experiment with it.

Requirements: Basic knowledge of logic and functional programming.

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] L. Lamport. How to Write a 21st Century Proof. Journal of Fixed Point Theory and Applications, 11:43–63, 2012.

[3] B. C. Pierce, A. Azevedo de Amorim, C. Casinghino, M. Gaboardi, M. Greenberg, C. Hritcu, V. Sjöberg, and B. Yorgey. Logical Foundations, volume 1 of Software Foundations. Electronic textbook, 2020. version 5.8.

[4] M. Wenzel. Isar - a generic interpretative approach to readable formal proof documents. In Proceedings of the 12th International Conference on Theorem Proving in Higher Order Logics, Lecture Notes in Computer Science 1690, 1999.

[5] M. Wenzel and F. Wiedijk. A comparison of the mathematical proof languages Mizar and Isar. Journal of Automated Reasoning, 29:389–411, 2002.


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