Internship subject: Developping a standard library for 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: This internship is about formal proofs, more specifically the development of a standard library on natural numbers, lists, etc. for the proof assistant Lambdapi.
Formal proofs are used in mathematics but also in the industry for certifying the correctness of protocols, software and hardware.
Lambdapi is a new proof assistant based on the λΠ-calculus [4] modulo rewriting [1]. Its specificity is to allow users to define functions, predicates and types bygeneral rewriting rules, that is, oriented equations [2].
As it was originally meant as a logical framework for translating proofs from one proof system to another one [1,3], it provides no standard library yet, which is not very convenient for new users.

Objectives: This internship aims at developing a basic standard library for Lambdapi providing users with elementary function definitions and formally checked proofs of lemmas on natural numbers, lists and vectors, by using the specificities of Lambdapi as much as possible.

Workplan: The intern will start by getting some familiarity with Lambdapi, before developing a standard library on natural numbers, lists and vectors, following for instance the standard libraries of MathComp (nat, seq), Coq or Agda.

Requirements: Basic knowledge of logic.

Possible followings: Considering more advanced data structures, including a hierarchy of mathematical algebraic structures (monoid, group, ring, etc.) using type classes.

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] G. Hondet and F. Blanqui. The New Rewriting Engine of Dedukti. In Proceedings of the 5th International Conference on Formal Structures for Computation and Deduction, Leibniz International Proceedings in Informatics 167, 2020.

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

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