Recherche

Je m'intéresse à la mécanisation des preuves mathématiques, en particulier en calcul formel.
Actuellement je termine une tactique pour Coq prouvant des inéquations polynomiales à coefficients réels, basée sur un algorithme dû à Hörmander. Assia Mahboubi commence une thèse sur ce sujet sous ma direction.
Je travaille aussi sur la traduction des preuves formelles en langue naturelle (avec Frédérique Guilhot, en lien avec le projet Mowgli).

La thèse d'habilitation à diriger des recherches (HDR) que je viens de soutenir,
et les transparents de la soutenance (27 novembre 2003).

En vrac

Un pre-print de C.Simpson, dans une base de pré-publications à Cornell.
Deux courtes preuves (1+1) de T.Coquand.
Le programme de Hilbert, d'après H.Lombardi.

L'action <<Calcul formel certifié>> 1998-2000