Coq (logiciel)

Un article de Wikipédia, l'encyclopédie libre.
Aller à : navigation, rechercher
Page d'aide sur l'homonymie Pour les articles homonymes, voir Coq (homonymie).
Coq (logiciel)
Image illustrative de l'article Coq (logiciel)
Logo

CoqIde : l'environnement de développement de Coq.
CoqIde : l'environnement de développement de Coq.

Développeurs INRIA, Université Paris Diderot, École polytechnique, Université de Paris XI, École normale supérieure de Lyon
Écrit en OCaml
Environnements Multiplate-forme
Langues Multilingue
Type Assistant de preuve
Licence GNU LGPL 2.1
Site web The Coq Proof Assistant

Coq est un assistant de preuve utilisant le langage Gallina, développé par l'équipe PI.R2 d'Inria au sein du laboratoire PPS du CNRS et en partenariat avec l'École polytechnique, le CNAM, l'Université Paris Diderot et l'Université de Paris XI (et antérieurement l'École normale supérieure de Lyon).

Le nom du logiciel (initialement CoC) est particulièrement adéquat car : il est français ; il est fondé sur le calcul des constructions (CoC abrégé en anglais) introduit par Thierry Coquand. Dans la même veine, son langage est Gallina et Coq possède un wiki dédié, baptisé Cocorico!.

Coq a été récompensé du ACM SIGPLAN Programming Languages Software 2013 Award.

Caractéristiques du logiciel[modifier | modifier le code]

Coq est donc fondé sur le calcul des constructions, une théorie des types d'ordre supérieur, et son langage de spécification est donc une forme de lambda-calcul typé. Le calcul des constructions utilisé dans Coq comprend directement les constructions inductives, d'où son nom de calcul des constructions inductives (CIC).

Coq a été récemment doté de fonctionnalités d'automatisation croissantes. Citons notamment la tactique Omega qui décide l'arithmétique de Presburger[1]

Plus particulièrement, Coq permet :

  • de manipuler des assertions du calcul ;
  • de vérifier mécaniquement des preuves de ces assertions ;
  • d'aider à la recherche de preuves formelles ;
  • de synthétiser des programmes certifiés à partir de preuves constructives de leurs spécifications.

C'est un logiciel libre distribué selon les termes de la licence GNU LGPL.

Parmi les grands succès de Coq, on peut citer:

Éléments du langage[modifier | modifier le code]

Exemple de programme[modifier | modifier le code]

  • La fonction factorielle :
Require Import Arith List Bool.
 
Fixpoint factorielle (x : nat) : nat :=
match x with
0 => 1
| S p => x * factorielle( p )
end.

Notes et références[modifier | modifier le code]

  1. L'arithmétique de Presburger, contrairement à l'arithmétique usuelle due à Peano est une théorie complète, c'est-à-dire que pour tout énoncé de son langage on peut décider si c'est un théorème de la théorie ou non (sa négation étant alors théorème). Cette arithmétique de Presburger, qui n'a pas d'axiomes pour la multiplication, échappe donc à l'incomplétude énoncée par théorème d'incomplétude.
  2. (en) « Feit-Thompson theorem has been totally checked in Coq », Msr-inria.inria.fr,‎ 2012-09-20 (consulté le 2012-09-25)
  3. Kepler avait-il raison ?Le Monde - 20/10/2014

Voir aussi[modifier | modifier le code]

Liens externes[modifier | modifier le code]