Sites Inria

English version

Julien Thèves, Citizen Press -

Coq : 30 années de travail d’équipe

Conçu il y a trente ans dans le laboratoire de Paris-Rocquencourt de l'INRIA, l’assistant de preuve Coq continue de mobiliser les équipes de recherche. Son développement continu témoigne de l’intérêt que lui porte la communauté scientifique, et maintenant le secteur économique.

1984 : Thierry Coquand , chercheur du projet Formel dirigé par Gérard Huet , pose dans sa thèse les bases d'un formalisme logique puissant appelé « Calcul des Constructions ». L'équipe développe alors un langage de programmation fonctionnel, Caml, et sur cette base commence la réalisation d'un environnement de développement de preuves dans le Calcul des Constructions, temporairement appelé « CoC », puis « Coq ». C'est le début d'une grande aventure scientifique, à laquelle vont contribuer au fil des années plusieurs générations de chercheurs, de l'INRIA mais aussi plus largement du milieu universitaire français.

En 1991, au sein de l'équipe Coq, Christine Paulin-Mohring poursuit le développement du logiciel sur la base d'un formalisme logique plus expressif : le Calcul des Constructions Inductives, puis prend le relais de Gérard Huet à la tête de l’équipe en 1996. « Coq a une longue histoire , rappelle Christine Paulin-Mohring. Dans les années 1990, des chercheurs comme Chet Murthy ou Jean-Christophe Filliâtre ont beaucoup contribué à sa réalisation.  » Aujourd’hui chercheur au sein de l’équipe Toccata et professeur à l’université Paris Sud, Christine Paulin-Mohring continue d’utiliser Coq régulièrement. « Coq est à la fois un langage de programmation et un langage de preuve mathématique. C’est sa grande force, estime-t-elle. En tant qu’informaticienne et mathématicienne, Coq m’offre le meilleur des deux mondes. C’est un outil pour aller au fond des choses. Il permet notamment de faire fonctionner nos ordinateurs dans de meilleures conditions, avec des programmes mieux construits.  »

De nombreux usages

Vers le début des années 2000, c’est Bruno Barras et Hugo Herbelin qui animent le développement de Coq. Signe de la notoriété de ce projet au sein d’Inria, il bénéficie d’une action de développement technologique : un dispositif qui vise à soutenir des projets transversaux et collaboratifs d’envergure, en lui allouant des moyens humains et techniques. Sous la houlette de Hugo Herbelin depuis 2006, plusieurs équipes Inria participent désormais au développement du logiciel : PI.R2 à Paris, Toccata à Orsay, mais aussi l'équipe Marelle dirigée par Yves Bertot et comprenant des chercheurs du laboratoire LIX à Palaiseau et du centre Sophia Antipolis d'Inria.

Au-delà de son développement, de nombreux scientifiques s’en servent quotidiennement dans le cadre de leurs recherches. C’est le cas de Daniel de Rauglaudre , ingénieur de recherche au sein de l’équipe Aoste. « Je m’appuie actuellement sur Coq pour prouver le théorème de Puiseux, qui permet de donner une description des solutions de certains type d’équations polynomiales. J’avance pas à pas car Coq exige d’être très rigoureux, précise-t-il. Le logiciel contrôle l’activité des mathématiciens et ne laisse passer aucune imprécision !  »

Le logiciel Coq sert également à vérifier la correction de logiciels vis-à-vis de leurs spécifications : il possède donc un grand intérêt pour les industriels et les services qui doivent certifier la sécurité de leurs systèmes informatiques. C'est ainsi qu'il a servi à certifier l'environnement Java Card des terminaux de paiement électronique par carte à puce (Trusted Logic, SUN, GEMALTO).

Mots-clés : Preuve Récompense SIGPLAN Programming Languages Software Award ACM SIGPLAN Coq

Haut de page

Suivez Inria