Mon domaine de recherche est la théorie des types, et en particulier son utilisation comme formalisme de fondations des mathématiques. Je m’intéresse en effet à la formalisation en pratique de résultats mathématiques sous la forme de bibliothèques numériques, au moyen de logiciels appelés assistants de preuve. Les assistants de preuve permettent en particulier de réduire la vérification de la correction des théorèmes à un procédé mécanique, effectué par un unique programme de confiance, le noyau de l’assistant de preuve.
Mais la formalisation des mathématiques est aussi un outil pour « faire » des mathématiques, et pas seulement les vérifier : étudier les analogies entre preuves, en découvrir de nouvelles, dégager des abstractions pertinentes,… Néanmoins, l’un des enjeux de la réalisation de ces bibliothèques est de combler le fossé qui sépare la langue utilisée pour dénoter les mathématiques dans la littérature ou les séminaires, de celle, considérablement plus rigoriste, qui permet de vérifier mécaniquement qu’un énoncé est bien formé et qu’une preuve est correcte. Pour y parvenir, il faut convoquer des techniques informatiques variées, issues de la théorie des langages de programmation, mais aussi de la théorie de la démonstration, de la preuve automatique, etc.
Équipe-projet Gallinette
Il s’agit du projet FRESCO (Fast and Reliable Symbolic Computation), dont l’objet est d’améliorer la fiabilité des résultats produits par les implémentations d’algorithmes de calcul formel. Aujourd’hui l’ordinateur est un instrument de recherche incontournable dans tous les domaines des mathématiques, même les plus abstraits. Il permet de formuler des conjectures mais aussi d’étayer des étapes de preuve. Mais la correction de ces calculs est souvent très difficile à vérifier. Nous voulons mettre au service des mathématiques calculatoires les récentes avancées spectaculaires des méthodes formelles, et en particulier la maturité acquise par les assistants de preuve.
Les systèmes de calcul formel et les assistants de preuves ont pour objectif commun de représenter et de manipuler en machine des objets mathématiques sophistiqués. Pourtant ces deux familles d’outils sont développées par des communautés disjointes, avec des motivations a priori différentes : la quête d’efficacité pour les premiers, celle de correction formelle pour les seconds. J’ai commencé à m’intéresser à la convergence entre ces deux points de vue au cours de ma thèse. Mais le contraste entre les succès récents des méthodes formelles dans des domaines comme la sécurité ou la compilation, et l’absence quasi-totale d’outils formellement vérifiés pour les mathématiques calculatoires m’a convaincue qu’il fallait s’atteler sérieusement à ce problème. Ensuite, de nombreuses discussions avec des collègues d’horizons scientifiques variés (calcul formel, théorie des nombres, arithmétique des ordinateurs, théorie des types,…) m’ont permis de mieux cerner la stratégie à adopter.
D’abord, une chance immense, et aussi le début d’une aventure enthousiasmante. Pouvoir bénéficier d’une telle bourse permet de ne plus se soucier du financement de nos recherches pendant un temps conséquent : c’est un luxe qui permet de se concentrer sur le projet scientifique lui-même. C’est aussi une forme de reconnaissance académique, et ce succès est en large part redevable à mes proches collègues, qui ont contribué à la mise au point de ce projet. En particulier, Guillaume Melquiond, chercheur de l'équipe-projet Toccata, en sera un collaborateur privilégié.
Par ailleurs, le projet FRESCO s’appuie sur l’assistant de preuve Coq, principalement développé par des chercheurs Inria depuis plus de 30 ans. Sans la qualité et la continuité du travail de ces développeurs, sans leur créativité et leur interaction suivie avec les utilisateurs, il n’aurait pas vu le jour.
Ce financement va nous permettre de consolider une équipe de chercheurs qui réunisse l'éventail requis de profils scientifiques.
Tous les membres de cette équipe pourront mettre simultanément leur expertise au service de la conception et de la réalisation d'un nouvel environnement de travail pour les mathématiques calculatoires. Cette simultanéité est un véritable atout.
Je n'ai pas de réponse à cette question. Cela dépend à la fois des avancées futures dans les domaines de recherche qui m'intéressent mais aussi, et peut-être surtout, des rencontres professionnelles que je serai amenée à faire.
