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
  • University of Nice, A.Dieudonné Laboratory: formalization of
    proofs in mathematics