Coq es un demostrador de teoremas interactivo lanzado por primera vez en 1989. Permite expresar afirmaciones matemáticas , verifica mecánicamente las pruebas de estas afirmaciones, ayuda a encontrar pruebas formales y extrae un programa certificado de la prueba constructiva de su especificación formal . Coq trabaja dentro de la teoría del cálculo de construcciones inductivas , un derivado del cálculo de construcciones . Coq no es un probador automático de teoremas, pero incluye tácticas ( procedimientos ) de prueba automática de teoremas y varios procedimientos de decisión .
La Association for Computing Machinery otorgó a Thierry Coquand , Gérard Huet , Christine Paulin-Mohring , Bruno Barras, Jean-Christophe Filliâtre, Hugo Herbelin, Chetan Murthy, Yves Bertot y Pierre Castéran con el premio ACM Software System Award 2013 para Coq.
Coq es un juego de palabras sobre el nombre de Thierry Coquand, Cálculo de construcciones o "CoC" y sigue la tradición francesa de nombrar las herramientas después de los animales ( coq en francés significa gallo). [3]
Cuando se ve como un lenguaje de programación, Coq implementa un lenguaje de programación funcional de tipo dependiente ; [4] cuando se ve como un sistema lógico, implementa una teoría de tipos de orden superior . El desarrollo de Coq ha sido apoyado desde 1984 por INRIA , ahora en colaboración con École Polytechnique , University of Paris-Sud , Paris Diderot University y CNRS . En la década de 1990, ENS Lyontambién fue parte del proyecto. El desarrollo de Coq fue iniciado por Gérard Huet y Thierry Coquand, y más de 40 personas, principalmente investigadores, han aportado características al sistema central desde sus inicios. El equipo de implementación ha sido coordinado sucesivamente por Gérard Huet, Christine Paulin-Mohring, Hugo Herbelin y Matthieu Sozeau. Coq se implementa principalmente en OCaml con un poco de C . El sistema central se puede ampliar mediante un mecanismo de complemento . [5]
El nombre coq significa " gallo " en francés y proviene de una tradición francesa de nombrar las herramientas de desarrollo de la investigación en honor a los animales. [6] Hasta 1991, Coquand estaba implementando un lenguaje llamado Cálculo de Construcciones y simplemente se llamaba CoC en ese momento. En 1991, se inició una nueva implementación basada en el Cálculo de Construcciones Inductivas extendido y se cambió el nombre de CoC a Coq en una referencia indirecta a Coquand, quien desarrolló el Cálculo de Construcciones junto con Gérard Huet y contribuyó al Cálculo de Construcciones Inductivas. con Christine Paulin-Mohring. [7]
Coq proporciona un lenguaje de especificación llamado Gallina [8] (" gallina " en latín, español, italiano y catalán). Los programas escritos en Gallina tienen la propiedad de normalización débil , lo que implica que siempre terminan. Ésta es una propiedad distintiva del lenguaje, ya que los bucles infinitos (programas que no terminan) son comunes en otros lenguajes de programación, [9] y es una forma de evitar el problema de las paradas .