This Research-Team is a follow-up of LEMME Research-Team
Project-Team Presentation
The goal of the MARELLE project-team is to study and use techniques for verifying mathematical proofs on the computer to ensure the correctness of software. The targeted domains consist in software for scientific computation (computer algebra, computer aritmetics). The project-team develops methods and tools to help producing correct program from precise descriptions of the data, the algorithms, their properties, and the proofs of these properties.
Research themes
- Proof development environments
- Formalization of mathematics and type theory
- Certified software
- Formal properties of numbers, exact arithmetics
International and industrial relations
- ANR Galapagos: Geometry, Algorithms, Proofs
- ANR Compcert: certified compiler
- ANR A3Pat: collaboration between rewriting and proving
- Microsoft-INRIA Institute: Mathematical components
- TYPES Working Group: computer-assisted reasoning based on type theory.
- University of Nice, A.Dieudonné Laboratory: formalization of proofs in mathematics
Scientific leader
Yves BERTOT
[homepage]
+33 4 92 38 77 39
Yves.Bertot@inria.fr
Secretary : +33 4 92 38 76 00
