Coq

Website: coq.inria.fr

CoQ este un prover interactiv al teoremei lansat pentru prima dată în 1989.

Permite exprimarea afirmațiilor matematice, verifică mecanic dovezile acestor afirmații, ajută la găsirea dovezilor formale și extrage un program certificat din dovada constructivă a specificațiilor sale formale.

CoQ lucrează în teoria calculului construcțiilor inductive, un derivat al calculului construcțiilor.

COQ nu este un prover automat al teoremei, dar include tactici (proceduri) și proceduri de decizie de dovedire automată.

Asociația pentru mașini de calcul acordate Thierry Coquand, Gérard Huet, Christine Paulin-Mohring, Bruno Barras, Jean-Christophe Filliți, Hugo Herbelin, Chetan Murthy, Yves Bertot și Pierre Castéran cu premiul Sistemului de software ACM 2013 pentru Coq.

Numele „Coq” este un joc de cuvânt pe numele lui Thierry Coquand, calculul construcțiilor sau „COC” și urmărește tradiția franceză de informatică a software -ului de denumire după animale (coq în franceză sensul cocoșului).