Sites Inria

English version

Mathilde De Vos -

Coq : 7 dates clefs

Le logiciel Coq reçoit le 23 janvier 2014 le SIGPLAN Programming Languages Software Award. Ce prix récompense chaque année un logiciel ayant eu un impact significatif dans la recherche ou le développement des langages de programmation. Le projet en 7 dates.

1984

Le travail de thèse de Thierry Coquand pose les bases du « Calcul des Constructions ». Cette théorie donnera naissance au développement de preuves dans le Calcul des Constructions : c'est le début de « CoC ».


1989

Première annonce publique. CoC était réservé jusqu'alors à quelques experts expérimentateurs.


1991

CoC est renommé Coq. Ce changement matérialise une évolution majeure du logiciel, l'introduction d'une nouvelle notion primitive d'objets appelés types inductifs. Cette notion universelle s'avère extrêmement naturelle en logique et en programmation. Ce changement fournit aussi des principes de récursion et d'induction primitifs, renonçant ainsi aux axiomes qui allaient à l'encontre des principes originels du Calcul des Constructions. La nouvelle version est donc purement calculatoire, basée sur une logique constructive. En clair, toute preuve est exécutable comme un programme.


1999

Nouvelle implémentation construite autour d'un noyau bien délimité. Ce noyau vérifie la correction logique, c'est lui qui assure les preuves : plus il est petit, plus il est fiable.


2004

Refonte de la syntaxe extérieure au noyau, uniformisation des bibliothèques. Le but est de permettre de nouvelles avancées. C'est le début de l'expansion pour Coq, notamment suite à la publication du Coq'Art, un ouvrage d'introduction écrit par Yves Bertot et Pierre Castéran .


2007

Coq permet la certification de propriétés du code de la Java Card à un degré absolu. Cela signifie qu'on accorde une confiance absolue à certaines fonctionnalités clés du système d'exploitation Java Card qu'utilisent de nombreuses cartes à puce (carte bleue, carte SIM, etc.)


2013

ACM SIGPLAN décerne le SIGPLAN Programming Languages Software Award à Coq, récompensant un projet de presque 30 ans. Le prix sera remis en main propre à San Diego en janvier 2014 à un comité composé de Gérard Huet , Yves Bertot , Jean-Christophe Filliâtre et Matthieu Sozeau .

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

Haut de page

Suivez Inria