Coq
Coq (gallo en francés) es un sistema de ayuda a la demostración de teoremas que maneja aserciones matemáticas, verifica mecánicamente las pruebas de aserciones, ayuda a encontrar prubas para esas aserciones y extrae programas certificados (correctos) a partir de las pruebas constructivas de aserciones que representan su especificación formal. Coq trabaja en base a la teoría del Cálculo de Construcciones Inductivas, que es una teoría derivada del Cálculo de Construcciones.
Enciclopedia Universal.
2012.