Dezvoltat de | INRIA , Diderot Universitatea din Paris , Școala Politehnică , Universitatea Paris-Sud , École Normale Supérieure de Lyon |
---|---|
Prima versiune | 1984 |
Ultima versiune | 8.13.1 (22 februarie 2021) |
Depozit | Cocos pe GitHub |
Starea proiectului | În dezvoltarea activă |
Scris in | OCaml |
Sistem de operare | Multiplatform |
Mediu inconjurator | Cross-platform |
Limbi | Engleză |
Tip | Asistent de dovadă |
Politica de distribuție | Free și open source |
Licență | GNU LGPL 2.1 |
Site-ul web | http://coq.inria.fr |
Coq este un asistent de probă care utilizează limbajul Gallina , dezvoltat de echipa PI.R2 din Inria în cadrul laboratorului PPS al CNRS și în parteneriat cu École Polytechnique , CNAM , Université Paris Diderot și Universitatea Paris-Sud (și anterior the École normale supérieure de Lyon ).
Numele software-ului (inițial CoC ) este deosebit de potrivit deoarece: este francez; se bazează pe calculul construcțiilor ( CoC prescurtat în limba engleză) introdus de Thierry Coquand . În același sens, limbajul său este Gallina și Coq are un wiki dedicat, numit Cocorico! .
Coq a primit premiul ACM SIGPLAN Programming Languages Software 2013 Award.
La începutul anilor 1980, Gérard Huet a inițiat un proiect pentru fabricarea unui demonstrator de teoreme interactive. Acesta este un asistent de probă. Thierry Coquand și Gérard Huet concep logica lui Coq și calculul construcțiilor. Christine Paulin-Mohring extinde această logică cu o construcție nouă, tipuri inductive și un mecanism de extracție care obține automat un program de eroare zero dintr-o dovadă.
Cocoșul se bazează pe proiectarea structurilor , o teorie a tipului de ordin superior , iar limbajul său de specificații este o formă de calcul lambda . Calculul construcțiilor utilizate în Coq include direct construcții inductive, de unde și numele său de calcul al construcțiilor inductive (CIC).
Coq a primit recent funcții de automatizare în creștere. Să cităm în special tactica Omega care decide aritmetica lui Presburger .
Mai precis, Coq permite:
Este un software gratuit distribuit în condițiile licenței GNU LGPL .
Printre marile succese ale Coq, putem menționa:
Cocoșul folosește corespondența Curry-Howard . Dovada unei propuneri este văzută ca un program al cărui tip este această propunere. Pentru a defini un program sau o dovadă, trebuie să:
De asemenea, este posibil să utilizați SSReflect în loc de Ltac. Fost dezvoltat separat, acum este inclus în mod implicit în Coq.