Sites Inria

Version française

MARELLE Research team

Mathematical, Reasoning and Software

  • Leader : Yves Bertot
  • Research center(s) : CRI Sophia Antipolis - Méditerranée
  • Field : Algorithmics, Programming, Software and Architecture
  • Theme : Proofs and Verification

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 domain concerns software for scientific computation (computer algebra, computer aritmetics). The project-team develops methods and tools to help producing correct program from precise descriptions of data, 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

Keywords: Formalization of mathematical algorithms Computer assisted proof