Nicolas Tabareau, ERC Starting Grant 2014

Alors qu’il s’intéressait au départ aux langages de programmation, Nicolas Tabareau mène maintenant des recherches dans le domaine de la preuve informatique.

Le projet prévu dans le cadre de son ERC Starting Grant, intitulé « CoqHoTT », s’appuie sur une récente découverte qui pourrait bouleverser les fondations théoriques utilisées par les logiciels de preuve informatique, tel Coq, et vise à développer un nouvel assistant de preuve.

La découverte en question est celle de Vladimir A. Voïevodski, mathématicien Russe et lauréat de la médaille Fields en 2002, qui a proposé un pont entre la théorie des types, qui est au cœur de l’assistant de preuve Coq, et la théorie de l’homotopie, c’est-à-dire la théorie de la déformation des espaces.

Les travaux de ce chercheur ont permis d’établir certaines limites du logiciel Coq, et de mettre en évidence plusieurs verrous scientifiques et technologiques. Pour le moment, il était possible de montrer que deux logiciels étaient identiques d’un point de vue sémantique, mais il persistait un frein à toute formalisation.

« Depuis 25 ans que les assistants de preuve sont développés, les verrous théoriques n’ont pas sauté. Jusqu’à récemment, on ne comprenait pas complétement pourquoi ce que l’on faisait "au tableau" ne pouvait pas toujours être facilement traduit dans le logiciel » explique Nicolas Tabareau.

Jusqu’à présent, les assistants de preuve étaient plutôt réservés à des personnes compétentes en informatique et en mathématiques, car il fallait pouvoir maîtriser les aspects théoriques du logiciel. Avec la nouvelle version envisagée, qui sera plus proche de ce que l’on peut apprendre à faire à l’école, il devrait être possible pour tout ingénieur de réaliser ce genre de formalisation.

L’idée de son projet est donc de développer une nouvelle version de Coq, plus facilement manipulable, en révisant ses aspects théoriques, et qui permette de mettre en œuvre plus facilement certains raisonnements.

Une quinzaine de chercheurs au niveau mondial s’intéressent actuellement à cette problématique. Il est encore difficile d’être sûr que ces travaux aboutiront. Certes les scientifiques ont beaucoup avancé depuis trois ans, autant au niveau théorique que sur le développement de l’outil, mais il y a déjà eu par le passé de mauvaises surprise en termes de développement logiciel. Actuellement, Nicolas Tabareau estime être « à mi-chemin entre l’inconnu et une possible solution. On sait où on veut aller, quel est l’objectif, mais nous ne sommes pas sûrs du chemin ». C’est d’ailleurs pourquoi son projet bénéficie d’une ERC Starting Grant, bourse dédiée à des projets de recherche pionniers et innovants. Nicolas Tabareau dispose ainsi d’une bourse de 5 ans pour constituer son équipe et conduire ses travaux.