Coq

Voir le site

Disponible sur

Mac OS X, Windows, GNU/Linux

Langues

English

Le logiciel Coq est un assistant à la preuve formelle développé à l’Inria. Il est fondé sur le Calcul des Constructions de Thierry Coquand, une théorie des types d’ordre supérieur, et exploite largement la correspondance de Curry-Howard. Coq peut manipuler des énoncés du calcul et permet de faire une vérification mécaniques de ces énoncés. Il peut aussi aider à la recherche de preuves formelles d’énoncés mathématiques (par exemple, le théorème des quatre couleurs) ainsi que à la vérification formelle de programmes informatiques (par exemple, le compilateur CompCert C).

Créateur·ices

Thierry Coquand

Licence(s)

Licence publique générale limitée GNU (LGPL)

Mots-clefs

science mathématiques

Liens externes

Fiche créée le Mardi, 3 mars, 2015 - 22:15
C'est quoi un mini-site ? Modifier cette notice