Projects and Interests
- EU STREP-FET-open FORMATH: This project proposes to develop libraries of formalized mathematics concerning algebra, linear algebra, real number computation, and algebraic topology.
- ANR PSI (with Stéphane Lengrand and Germain Faure): This project is funded by the ANR (French National Research Agency) action for junior researchers. This project aims at investigating how to take into account the specificities of a given theory when designing proof search methods, both in the theory of proof search and in the design of automated tools.
- ANR DeCert (national consortium): This project aims at building trustworthy verification tools based on the collaboration of SMT-like decision tools and proof assistants.
- INRIA Microsoft Research Joint Centre: I' am a member of the Mathematical Components Project, lead by Georges Gonthier. This project is investigating the art of building formal libraries. It aims at demonstrating that software ingeneering methods can apply to formalized mathematics and to show how. Our main goal is to achieve a formal proof of the Feit-Thompson theorem. This page shows the current state of the formalization and that one shows the documentation of the corrresponding libraries.
Publications
I now let HAL maintain my list of publications. Some other written stuff, older or not available through the previous link:- Packaging Mathematical Structures, F. Garillot, G. Gonthier, L. Rideau, (accepté à TPHOLs2009, disponible ici).
- Implementing the CAD algorithm inside the Coq system, (Mathematical Structures in Computer Sciences 17(1) 2007, pdf)
- Programming and certifying the CAD in the Coq system ( Dagsthul seminar proceedings), .pdf,
- Proving equalities in a commutative ring done right in Coq, Benjamin Grégoire, Assia Mahboubi (TPHOL2005).ps
- An induction principle over real numbers (to appear in Archive for Mathematical Logic) .ps
- Un principe d'induction pour les réels (master degree internship) .ps
- Elimination des quantificateurs sur les réels en Coq, Assia Mahboubi, Loïc Pottier (in french).JFLA 2002 .ps