Coq

Rocq (prèviament conegut com Coq) és un sistema d'ajuda per a la demostració de teoremes que maneja asserció matemàtiques, verifica mecánicamente les proves de asserció, ajuda a trobar proves per a eixes asserció i extrau programes certificats (correctes) a partir de les proves constructives de asserció que representen la seua especificació formal. Rocq treballa basant-se en la teoria del Càlcul de Construccions Inductivas, que és una teoria derivada del Càlcul de Construccions.

Va ser desenrollat en França, en el proyecte LogiCal, entre l'INRIA, l'École Polytechnique, l'Universitat París XI i el CNRS. Dirigixen el desenroll els investigadors Gilles Dowek i Christine Paulin-Mohring. Coq està escrit en el llenguage OCaml.

Este artícul conté una traducció derivada de «Coq» de Wikipedia en castellà publicada baix la Llicència de documentació lliure de GNU i la Llicència Creative Commons Reconeiximent-CompartirIgual 4.0 Internacional.