Sites Inria

English version

Logiciel

Une action de développement technologique pour Coq

L'action de développement technologique (ADT) Coq regroupe les personnes et équipes participant collectivement à l'implantation du logiciel d'aide à la preuve Coq.

Il est utilisé internationalement par le monde académique dans des applications telles que l’enseignement, la spécification des langages de programmation ou la formalisation des mathématiques. La démonstration du théorème des quatre couleurs avec Coq en est un exemple célèbre. Il est un outil clé pour les sociétés comme Gemalto et Trusted Logic qui ont besoin de garantir de hauts niveaux de sécurité pour des applications comme le paiement par carte bancaire sur Internet.

La maintenance du logiciel est principalement le fait des chercheurs de l’Inria répartis sur trois centres à Paris-Rocquencourt (PI.R2), Saclay (Typical, Proval) et Sophia Antipolis (Marelle). « Le fait d’être sur plusieurs sites rend les contacts plus difficiles et c’est ce qui nous a poussé à demander une action de développement technologique (ADT) » explique Hugo Herbelin, coordonnateur de l’ADT Coq. « Elle nous fournit des moyens supplémentaires et a mis à notre disposition deux ingénieurs pour travailler sur l’interface graphique et l’interface avec d’autres outils. Cela permet d’officialiser ce développement multisite et de lui assurer une continuité. »

Mots-clés : Coq Logiciel Paris - Rocquencourt

Haut de page

Suivez Inria