Sites Inria

Version française

LEMME Research team

Activity reports

Overall Objectives

Formal methods have become increasingly important in software development. The Lemme project aims at contributing to their use in software construction and scientific computing. In particular, we try to bridge the gap between solving a mathematical problem on paper and using a computer, as the latter supports and requires many mechanical computations. Special attention is given to logical consistency and the ease of transfer from theory to practice.

To reach our goal, we work on the following themes:

formalization of mathematical theories describing the basic objects of scientific knowledge;

development of tools to facilitate the construction of mathematical proofs and efficient implementations, derived from the formal description of an algorithm and its correctness proof; and

formalization of programming language semantics;

development of the user's working environment in which the certified algorithms and the corresponding proofs are developed. Users can be, for example, researchers, engineers, or students.

Although these themes could have a life of their own, they strongly influence each other. The researcher's working environment needs efficient and correct proof tools. Developing these tools requires the certified description of algorithms, which in turn requires formalizing the basic mathematical tools. Once algorithms are described, it is necessary to implement them in a programming language, whose semantics must be mastered. To complete the circle, formalizing mathematics or programming language semantics can be done more easily and efficiently thanks to a practical working environment.