Je m'intéresse actuellement à la mécanisation des preuves mathématiques.  Ma page web la plus récente est ici.^[1]

février 2012: début du cours de logique en MAM3 de Polytech’Nice. La page du cours est ici.

novembre 2011: les transparents du mini-cours “Preuves formelles automatiques en géométrie” aux JNCF 2011: partie 1, partie 2. Demo. Le cours sera publié ici.

août 2011: voici les tactiques nsatz, cring et non_commutative_ring reprises en utilisant au maximum les classes de types: nsatz-8.3pl2.tgz,  setoid_ring-8.3pl2.tgz.

On peut facilement les utiliser avec Ssreflect, voici un exemple avec des matrices.

avril 2011: en reprenant du vieux code sur les téléscopes, voilà un début de généralisation des structures algébriques utilisant les classes de types.

31 mars 2011: GT Coq sur la réification: manifestement, l’équipe de Bas Spitters a fait un travail bien plus poussé que le mien sur l’utilisation des classes de types en Coq, et je vais m’en inspirer pour améliorer mes tactiques nsatz et rings. Après avoir discuté avec Assia, je crois avoir compris que les canonical structures avaient la puissance des classes de types moins le backtrack complet.

mars 2011: évaluation de l’équipe Marelle; groupe de travail Coq sur la réification, voilà mes transparents.

février 2011: reprise de la tactique ring, cas commutatif ou non, avec réification par les Type Classes, du coup plus besoin de code ml. Je continue avec les algèbres.

janvier 2011: écriture d'une tactique Coq pour les polynômes non commutatifs (algèbres de Weyle, D-modules, etc). Je commence à la fin du mois un cours de logique en MAM3 à Polytech'Nice.

décembre 2010: étude et simplification de la preuve d'extentionnalité de V.Voevodsky.

juin 2010: intégration de la tactique nsatz à Coq (trunk), qui prouve des équations polynomiales; examen de logique Polytech'Nice MAM3.

avril 2010: expérimentation des Type Classes de Mathieu Sozeau dans la version 8.3béta de Coq, et, ma foi, ça a l'air très puissant pour formaliser confortablement des maths: surcharge, sous-types, quotients.

En 2008-2009, j'ai écrit des tactiques pour Coq qui démontrent des équations polynomiales (par le Nullstellensatz et à l'aide de bases de Gröbner) (article). Avec Benjamin Grégoire et Laurent Théry, nous avons utilisé la dernière tactique pour produire des certificats courts de théorèmes de géométrie (article et exemples sur le web).

Puis j'ai expérimenté une compilation de Coq en C et je l'ai comparée à la compilation en code natif (ocamlopt) du code produit par l'extraction de Coq. Le résultat n'est pas suffisamment concluant pour poursuivre cette voie. 

Auparavant, entre 2004 et 2008, j'ai passé pas mal de temps à développer et expérimenter des interfaces pour faire faire des preuves par des étudiants avec André Hischowitz et ses collègues enseignants du département de mathématiques à Nice (article). J'ai aussi participé au mouvement "Sauvons la recherche", sans grand résultat, mais il fallait bien, cela faisait partie de mon travail de chercheur. 300 postes ont tout de même été sauvés en juin 2004.

Encore avant, je me suis intéressé à certifier des calculs formels (= algébriques) à l'aide de Coq, et j'ai dirigé une équipe (Lemme, on disait "projet"), passé pas mal de temps dans des commissions (membre nommé au Conseil National des Universités , élu SNTRS-CGT à la commission d'évaluation de l'INRIA, jurys de recrutements divers) à l'époque où ce n'était pas rémunéré. Mais encore une fois cela faisait partie de mon travail de chercheur.

Quand je ne connaissais pas encore Coq, je m'occupais :-) avec des problèmes de combinatoire algébrique: bases de Gröbner toriques, équations diophantiennes linéaires, bornes de complexité, algorithme d'Euclide en dimension quelconque. 

J'ai dirigé quelques thèses (Assia Mahboubi, Laurent Chicli, Stéphane Lavirotte, Catherine Moulinet, Christèle Faure) et pas mal de stages (Cody Roux, Benjamin Grégoire, Virgile Prévosto, pardon pour les nombreux autres, je n'ai pas la mémoire des noms et mes archives au bureau ont disparu dans un incendie). Tout ça est détaillé dans mon mémoire d'habilitation.

Je ne suis pas intéressé par: les primes. Je trouve ça plutôt dé-primant ;-)

Publications

La dernière:  Proof certificates for algebra and their application to automatic geometry theorem proving Benjamin Grégoire, Loïc Pottier, Laurent Théry, accepté dans les post-proceedings LNAI de ADG2008, vol 6301, à paraître en 2011

Toutes

Exposés

Journées Nationales de Calcul Formel, novembre 2011: mini-cours de 3h sur les preuves formelles, démo de Coq.

DECERT, janvier 2009.

Enseignement

Cette année, comme les deux années passées, de février à mai je donne un cours de logique niveau L3 à Polytech'Nice. Les TD sont faits en Coq.

Depuis quelques années, je m'occupais d'un groupe de TD de sémantique en M1 informatique à l'université de Nice (le cours est fait par Yves Bertot). Avant j'y faisais un cours de lambda-calcul.

En 2003-2006, j'avais donné un cours sur les preuves formelles en DEA/M2 de mathématiques à Nice.

De 1991 à 2001, j'assurais un cours de logique en maîtrise de mathématiques à l'université de Nice, qui s'était orienté d'année en année vers le lambda-calcul et les preuves formelles en Coq.