Coq

Coq is een interactieve stellingbewijzer die voor het eerst werd uitgebracht in 1989. Het maakt het uitdrukken van wiskundige beweringen mogelijk, het controleert mechanisch de bewijzen van deze beweringen, het helpt bij het vinden van wiskundige bewijzen en het extraheert een gecertificeerd programma uit het constructieve bewijs van de formele specificatie ervan. Coq werkt binnen de theorie van de calculus van inductieve constructies, een afgeleide van de calculus van constructies. Coq is geen geautomatiseerde stellingbewijzer, maar omvat automatische stellingenbewijstactieken (procedures) en verschillende beslissingsprocedures. De Curry-Howard-correspondentie is de directe relatie tussen computerprogramma's en wiskundige bewijzen.

De naam "Coq" is een woordspeling op de naam van Thierry Coquand, Calculus of Constructions of "CoC" en volgt de Franse computerwetenschappelijke traditie van het vernoemen van software naar dieren (coq betekent in het Frans haan). Het ontwikkelingsteam maakte op 11 oktober 2023 bekend dat de naam Coq de komende maanden in The Rocq Prover zal worden veranderd.