Coq (logiciel)
Pour les articles homonymes, voir Coq (homonymie).
  |
Vous pouvez partager vos connaissances en l’améliorant (comment ?) selon les recommandations des projets correspondants.
|
| Coq (logiciel) | |
 Logo |
|
|
|
|
 |
|
|
|
|
| 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 |
modifier  |
|
Coq est un assistant de preuve utilisant le langage Gallina, développé par l'équipe PI.R2 de l'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).
Sommaire |
Caractéristiques du logiciel [modifier]
Coq est fondé sur le calcul des constructions (introduit par Thierry Coquand, CoC abrégé en anglais, d'où un jeu de mots justifiant le nom du système), 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:
- théorème des quatre couleurs: la démonstration complètement mécanisée a été terminée en 2004 par Georges Gonthier et Benjamin Werner.
- Théorème de Feit et Thompson: la preuve du théorème a été terminée par Georges Gonthier et son équipe en septembre 2012[2].
- CompCert un compilateur optimisant le C (langage) qui est entièrement programmé et prouvé en Coq.
Éléments du langage [modifier]
Exemple de programme [modifier]
- 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]
- 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.
- (en) Feit-Thompson theorem has been totally checked in Coq, Msr-inria.inria.fr, 2012-09-20. Consulté le 2012-09-25
