Projets et Intérêts
- EU STREP-FET-open FORMATH : Ce projet Européen propose de développer des bibliothèques de mathématiques formaliséees en algèbre, algèbre linéaire, géométrie algébrique réelle, topologie algébrique et calcul sur les réels.
- ANR PSI (avec Stéphane Lengrand et Germain Faure): Ce projet est un projet ANR JCJC. Il a pour but de comprendre comment prendre en compte les spécificités d' une théorie cible particulière lors de l'élaboration de stratégies de recherches de preuve, à la fois au niveau de la théorie de la démonstration mais aussi dans le design d' outils automatiques.
- ANR DeCert (consortium national): Ce projet a pour but de développer des outils fiables de vérification, basés sur la collaboration d'outils de décision de la famille SMT avec des assistants à la preuve.
- Centre commun INRIA Microsoft Research: Je fait partie de l'équipe Composants Mathématiques, dirigé par Georges Gonthier. Ce projet explore l'art de réaliser des bibliothèques formelles. Il a pour but de prouver que les méthodes de génie logiciel s'appliquent au domaine de la formalisation de mathématiques, et de montrer comment. L'objectif est de mettre en oeuvre ces méthodes en réalisant une preuve formelle du théorème de Feit-Thompson. Cette page affiche l'état courant de la formalisation et celle-ci la documentation des bibliothèques correspondantes.
Publications
Je laisse maintenant HAL maintenir à jour ma liste de publications. Des choses plus anciennes ou non disponibles à travers le précédent lien:- 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