- Presentation
- HAL publications
- Activity reports
MARELLE Research team
Mathematical, Reasoning and Software
- Leader : Yves Bertot
- Type : Project team
- Research center(s) : Sophia
- 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
Research teams of the same theme :
- ANTIQUE - Static Analysis by Abstract Interpretation
- CELTIQUE - Software certification with semantic analysis
- CONVECS - Construction of verified concurrent systems
- DEDUCTEAM - DEDUCTEAM
- GALLINETTE - GALLINETTE
- GALLIUM - Programming languages, types, compilation and proofs
- MEXICO - Modeling and Exploitation of Interaction and Concurrency
- MOCQUA - Designing the Future of Computational Models
- PARSIFAL - Proof search and reasoning with logic specifications
- PI.R2 - Design, study and implementation of languages for proofs and programs
- SUMO - SUpervision of large MOdular and distributed systems
- TOCCATA - Certified Programs, Certified Tools, Certified Floating-Point Computations
- VERIDIS - Modeling and Verification of Distributed Algorithms and Systems
Contact
Team leader
Yves Bertot
(See all teams)
Tel.: +33 4 92 38 77 39
Secretariat
Tel.: +33 4 92 38 76 00
Find out more
Genealogy
This team follows