Coq (logiciel)
assistant de preuve / De Wikipedia, l'encyclopédie encyclopedia
Cher Wikiwand IA, Faisons court en répondant simplement à ces questions clés :
Pouvez-vous énumérer les principaux faits et statistiques sur Coq (assistant de preuve)?
Résumez cet article pour un enfant de 10 ans
Pour les articles homonymes, voir Coq (homonymie).
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é Paris-Sud (et antérieurement l'École normale supérieure de Lyon).
Cet article est une ébauche concernant les mathématiques et un logiciel libre.
Vous pouvez partager vos connaissances en l’améliorant (comment ?) selon les recommandations des projets correspondants.
Développé par | INRIA, Université Paris Diderot, École polytechnique, Université Paris-Sud, École normale supérieure de Lyon |
---|---|
Première version | |
Dernière version | 8.19.1 ()[1] |
Dépôt | Coq sur GitHub |
État du projet | En développement actif |
Écrit en | OCaml et C |
Système d'exploitation | Multiplateforme |
Langues | Anglais |
Type | Assistant de preuve |
Politique de distribution | Gratuit et open source |
Licence | GNU LGPL 2.1 |
Site web | coq.inria.fr |
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!.
En 2013, Coq a été récompensé du Programming Languages Software Award par l'ACM SIGPLAN[2]. Coq a reçu en 2022 le premier prix science ouverte du logiciel libre de la recherche dans la catégorie « scientifique et technique »[3].