Back Coq (Software) German Coq Greek Coq (software) English Coq Spanish Coq Finnish Coq Japanese Coq Dutch Coq Portuguese Coq Russian Coq Ukrainian
Pour les articles homonymes, voir Coq (homonymie).
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.2 ()[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 |
Coq est un assistant de preuve utilisant le langage Gallina, développé par l'équipe PI.R2[2] 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).
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[3]. Coq a reçu en 2022 le premier prix science ouverte du logiciel libre de la recherche dans la catégorie « scientifique et technique »[4].
- « Release Coq 8.19.2 », (consulté le )
- « Bienvenue », sur univ-paris-diderot.fr (consulté le ).
- « Programming Languages Software Award » (consulté le )
- « Remise des prix science ouverte du logiciel libre de la recherche », (consulté le )
© MMXXIII Rich X Search. We shall prevail. All rights reserved. Rich X Search