|
project
Mathematical Components
New!
Download the latest release of the Ssreflect extension.
Project Summary
 The object of this project is to demonstrate that formalized mathematical theories can, like modern software, be built out of components. By components we mean modules that comprise both the static (objects and facts) and dynamic (proof and computation methods) contents of theories. We propose to develop a general platform for mathematical components, based on the Coq “Ssreflect” extension that was used to carry out the formalization of the Four Colour Theorem. We would validate the platform on two significant developments: a theory of efficient arithmetic, and the proof of the Odd Order theorem. The former could be used in the resolution of several outstanding computer proof challenges, among them the Kepler Conjecture, and the latter could become the first step in a new major challenge: the classification of finite simple groups.
Research Team
The project is based at two locations
Orsay
- Jeremy Avigad, Carnegie Mellon University
- Bruno Barras, INRIA Researcher, team TypiCal
- Cyril Cohen, PhD student
- François Garillot, PhD Student
- Georges Gonthier (team leader), MSR Cambridge Senior Researcher
- Assia Mahboubi, INRIA Researcher, team TypiCal
- Enrico Tassi, PostDoc researcher
- Benjamin Werner (arithmetic leader), INRIA Researcher, team TypiCal
Sophia Antipolis
Former Members
Current state of the project
Get a coqdoc snapshot of the development on this web page.
Download the Ssreflect extension for the Coq system
New Version 1.2 !
We are pleased to announce the latest full release of the Ssreflect extension library for the Coq proof assistant, version 8.2pl1.
Ssreflect version 1.2 is distributed under either one (your choice) of the CeCILL B or CeCILL 2 license (the French equivalents of the BSD and GNU/GPL license, respectively).
Earlier versions
- Ssreflect version 1.1, for the Coq proof assistant, version 8.1. Distributed under the CeCILL B license (the French equivalent of the BSD license): Download
- Ssreflect version 1.0, for the Coq proof assistant, version 8.0. Distributed as an MSR distribution: Download
The Ssreflect documentation
The Reference Manual of the extension is available here, as an INRIA Research report.
The Ssreflect users discussion list
Comments and bug reports on the Joint Centre distribution of Ssreflect are of course most welcome, and can be directed at ssreflect(at-sign)msr-inria.inria.fr ( subscribe, unsubscribe).
Publications
- Formal verification of exact computations using Newton's method, N. Julien, I. Pasca (accepted for publication at TPHOLs2009, available as an INRIA Research Report)
- Packaging Mathematical Structures, F. Garillot, G. Gonthier, A. Mahboubi, L. Rideau (accepted for publication at TPHOLs2009, available as an INRIA Research Report)
- Finite groups representation theory with Coq, S. Ould Biha (accepted for publication at MKM2009, available as an INRIA Research Report)
- Canonical Big Operators, Y. Bertot, G. Gonthier, S. Ould Biha, I. Pasca (TPHOLs2008, available as an INRIA Research Report)
- Formalisation des mathématiques : une preuve du théorème de Cayley-Hamilton, S. Ould Biha (JFLA 2008, in french)
- A Formal Verification for Kantorovitch's Theorem, I. Pasca (JFLA 2008)
- A Modular Formalisation of Finite Group Theory, G. Gonthier, A. Mahboubi, L. Rideau, L. Théry, E. Tassi (TPHOLs2007, available as an INRIA Research report)
- A Small Scale Reflection Extension for the Coq system, G. Gonthier, A. Mahboubi (INRIA Research Report)
- Our manifesto
Events
|
