Accueil > Présentation > Prix et distinctions > ERC starting Grant

ERC starting Grant

Nicolas Tabareau, chargé de recherche Inria et membre de l’équipe ASCOLA, est lauréat d’un ERC starting Grant dédié aux jeunes chercheurs pour le projet CoqHoTT.

CoqHoTT signifie Coq for Homotopy Type Theory.

Le but de ce projet est 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 performant, comme Coq développé au sein d’Inria.

CoqHoTT se base sur la découverte récente par un lauréat de la médaille Field, Vladimir Voevosdky, du lien fort entre la théorie de l’homotopie (qui étudie la notion de déformation continue en topologie) et la théorie des types (qui est au cœur de l’assistant de preuve Coq).

L’objectif principal de CoqHoTT est de fournir une nouvelle génération d’assistants de preuve sur la base de cette connexion fascinante.

Dernière modification : lundi 5 janvier 2015