Coq (logiciel)

Un article de Freepedia.

Cet article est une ébauche à compléter concernant l'informatique, vous pouvez partager vos connaissances en le modifiant.

Image:Math.png

Cet article est une ébauche à compléter concernant les mathématiques, vous pouvez partager vos connaissances en le modifiant.

Coq est un assistant de preuve développé à l'INRIA, à l'École polytechnique et à l'Université de Paris XI (et antérieurement à l'École normale supérieure de Lyon) dans le cadre du projet LogiCal ([1]).

Coq est basé 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.

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.

Parmi les grands succès de Coq, on peut citer la démonstration complètement mécanisée du théorème des quatre couleurs par Georges Gonthier et Benjamin Werner.