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 by general 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.

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