 | |
| Desarrollador (es) | El equipo de desarrollo de Coq |
|---|---|
| Versión inicial | 1 de mayo de 1989 (versión 4.10) |
| Lanzamiento estable | 8.13.0 [1] / 7 de enero de 2021 |
| Versión de vista previa | 8.13 + beta1 [2] / 7 de diciembre de 2020 |
| Repositorio | github |
| Escrito en | OCaml |
| Sistema operativo | Multiplataforma |
| Disponible en | inglés |
| Tipo | Asistente de pruebas |
| Licencia | LGPLv2.1 |
| Sitio web | coq |
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 de teoremas automatizado, pero incluye tácticas ( procedimientos ) de demostración 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 lleva el nombre de su desarrollador principal, Thierry Coquand. [ cita requerida ]
Resumen [ editar ]
Cuando se ve como un lenguaje de programación, Coq implementa un lenguaje de programación funcional de tipo dependiente ; [3] 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 . [4]
El nombre coq significa " gallo " en francés y proviene de la tradición francesa de nombrar las herramientas de desarrollo de la investigación en honor a los animales. [5] 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. [6]
Coq proporciona un lenguaje de especificación llamado Gallina [7] (" 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, [8] y es una forma de evitar el problema de las paradas .
Teorema de los cuatro colores y extensión SSReflect [ editar ]
Georges Gonthier de Microsoft Research en Cambridge , Inglaterra y Benjamin Werner de INRIA utilizaron Coq para crear una prueba encuestable del teorema de los cuatro colores , que se completó en 2005. [9] Su trabajo condujo al desarrollo de SSReflect ("Small Scale Reflection ") paquete, que fue una extensión significativa de Coq. [10] A pesar de su nombre, la mayoría de las características agregadas a Coq por SSReflect son características de propósito general y no se limitan al estilo de prueba de reflexión computacional. Estas funciones incluyen:
- Notaciones convenientes adicionales para una coincidencia de patrones irrefutable y refutable , en tipos inductivos con uno o dos constructores
- Argumentos implícitos para funciones aplicadas a argumentos cero, lo cual es útil cuando se programa con funciones de orden superior
- Argumentos anónimos concisos
- Una
settáctica mejorada con un emparejamiento más poderoso - Apoyo a la reflexión
SSReflect 1.11 está disponible gratuitamente, tiene doble licencia bajo la licencia de código abierto CeCILL-B o CeCILL-2.0, y es compatible con Coq 8.11. [11]
Aplicaciones [ editar ]
- CompCert : un compilador de optimización para casi todo el lenguaje de programación C que está en gran parte programado y probado en Coq.
- Estructura de datos de conjuntos disjuntos : la prueba de corrección en Coq se publicó en 2007. [12]
- Teorema de Feit-Thompson : la demostración formal con Coq se completó en septiembre de 2012. [13]
- Teorema de los cuatro colores : la demostración formal con Coq se completó en 2005. [9]
Ver también [ editar ]
- Nuprl
- Agda
- Idris
- Cálculo de construcciones
- Correspondencia Curry-Howard
- Isabelle (asistente de pruebas) - software similar / competidor
- Teoría de tipos intuicionistas
- HOL (asistente de pruebas)
Referencias [ editar ]
- ^ "Coq 8.12.2 está fuera" . 2020-12-11.
- ^ "Coq 8.13 + beta1 está fuera" . 2020-12-07.
- ^ Una breve introducción a Coq
- ^ Avigad, Jeremy; Mahboubi, Assia (3 de julio de 2018). Demostración interactiva de teoremas: 9a Conferencia Internacional, ITP 2018, celebrada como ... ISBN 9783319948218. Consultado el 21 de octubre de 2018 .
- ^ "Preguntas frecuentes" . Consultado el 8 de mayo de 2019 .
- ^ "Introducción al cálculo de construcciones inductivas" . Consultado el 21 de mayo de 2019 .
- ^ Adam Chlipala. "Programación certificada con tipos dependientes": "Universos de biblioteca" .
- ^ Adam Chlipala. "Programación certificada con tipos dependientes": "Library GeneralRec" . "Library InductiveTypes" .
- ^ a b Gonthier, Georges (2008), "Prueba formal: el teorema de los cuatro colores" (PDF) , Avisos de la American Mathematical Society , 55 (11), págs. 1382-1393, MR 2463991
- ^ Georges Gonthier, Assia Mahboubi. "Una introducción a la reflexión a pequeña escala en Coq": "Revista de razonamiento formalizado" .
- ^ "La biblioteca de componentes matemáticos 1.11.0" .
- ^ Conchon, Sylvain; Filliâtre, Jean-Christophe (octubre de 2007), "A Persistent Union-Find Data Structure", Taller ACM SIGPLAN sobre ML , Freiburg, Alemania
- ^ "El teorema de Feit-Thompson se ha comprobado totalmente en Coq" . Msr-inria.inria.fr. 2012-09-20. Archivado desde el original el 19 de noviembre de 2016 . Consultado el 25 de septiembre de 2012 .
Enlaces externos [ editar ]
 | Wikimedia Commons tiene medios relacionados con Coq . |
- El asistente de pruebas de Coq : el sitio web oficial en inglés
- coq / coq : el repositorio de código fuente del proyecto en GitHub
- Sistema interactivo en línea JsCoq : permite ejecutar Coq en un navegador web, sin necesidad de instalar ningún software.
- Alectryon : una biblioteca para procesar fragmentos de Coq incrustados en documentos, que muestra objetivos y mensajes para cada oración de Coq
- Wiki Coq
- Biblioteca de componentes matemáticos : biblioteca de estructuras matemáticas ampliamente utilizada, parte de la cual es el lenguaje de prueba SSReflect
- Repositorio de Coq constructivo en Nijmegen
- Clases de Matemáticas
- Coq en Open Hub
- Libros de texto
- The Coq'Art - un libro sobre Coq de Yves Bertot y Pierre Castéran
- Programación certificada con tipos dependientes : libro de texto en línea e impreso de Adam Chlipala
- Fundamentos de software : libro de texto en línea de Benjamin C. Pierce et al.
- Una introducción a la reflexión a pequeña escala en Coq : un tutorial sobre SSReflect por Georges Gonthier y Assia Mahboubi
- Tutoriales
- Introducción al asistente de pruebas de Coq : conferencia en video de Andrew Appel en el Instituto de Estudios Avanzados
- Tutoriales en vídeo para el asistente de pruebas Coq de Andrej Bauer.
