Informatique : « CoqHoTT » séduit l’European Research Council (ERC)

Nicolas Tabareau, chargé de recherche Inria au sein de l’équipe Ascola*, basée à Mines Nantes, a décroché une bourse de l’European Research Council (ERC) dans la catégorie « starting » avec son projet « CoqHoTT » : 1,5 million sur 5 ans pour constituer son équipe et conduire ses travaux de recherche en informatique.

L’European Research Council (ERC) fait partie intégrante du premier pilier « Excellence scientifique » du nouveau Programme de Recherche et d’Innovation de la Commission européenne : Horizon 2020. Il est chargé de coordonner les efforts de la recherche entre les états membres en soutenant les carrières de chercheurs indépendants excellents, dans tous les domaines scientifiques. L’ERC soutient trois types de chercheurs : ceux qui sont en début de carrière, ERC « starting » (jusqu’à 7 ans après avoir obtenu leur doctorat), « consolidator » (jusqu’à 14 ans), et « advanced » (pour les plus expérimentés). La bourse décrochée par Nicolas Tabareau, chargé de recherche au département informatique de Mines Nantes, entre dans la première catégorie.

Vers une nouvelle génération d’assistants de preuves

« CoqHoTT » pour Coq for Homotopy Type Theory a pour but d’aller plus loin dans la correspondance entre preuves et programmes qui a déjà permis ces 20 dernières années de développer des assistants de preuves performants, comme Coq développé au sein d’Inria. « Depuis le crash d’Ariane 5 dû à un bogue informatique évitable, l’industrie a compris l’importance d’avoir des logiciels certifiés. Un assistant de preuve est un logiciel permettant l’écriture et la vérification de preuves mathématiques, soit sur des théorèmes, soit sur des assertions relatives à l’exécution de programmes informatiques », explique Nicolas Tabareau. « Les assistants de preuves basés sur une correspondance entre preuves et programmes (comme Coq) permettent de prouver des propriétés de correction pour des programmes très complexes. Le compilateur du projet CompCert par exemple contient une preuve que le programme compilé se comporte exactement comme le programme C initial. » Coq est aussi utilisé pour formaliser des preuves de théorèmes mathématiques quand celles-ci sont trop longues et complexes pour être vérifiées à la main. « La preuve du théorème des 4 couleurs dans sa version initiale faisait plusieurs milliers de pages avec des centaines de cas complexes. Coq a permis d’automatiser la preuve de la plupart de ces cas et de transformer ces milliers de pages en un programme exécutable pour vérifier que le théorème est correct. »

Avec « CoqHoTT », Nicolas Tabareau envisage de fournir une nouvelle génération d’assistants de preuve sur la base de la découverte récente effectuée par Vladimir Voevosdky, lauréat de la médaille Field, du lien fort entre la théorie de l’homotopie (qui étudie la notion d’espace topologique) et la théorie des types (qui formalise la correspondance entre preuves et pro grammes au coeur de l’assistant de preuve Coq). Ce projet, porté par Inria, est programmé sur 5 ans (2015-2020).

*L’équipe de recherche ASCOLA est commune à Inria, Mines Nantes, l’Université de Nantes et le CNRS, au Laboratoire d’Informatique Nantes Atlantique (LINA).

Lire le communiqué de presse