Coq

Este programa tiene muy interesantes aplicaciones en diversos campos, ya que podemos utilizarla desde el área de la enseñanza de las matemáticas al entorno industrial. Coq es un sistema de demostración que nos proporciona un lenguaje formal para escribir definiciones matemáticas, algoritmos ejecutables y teoremas, todo ello junto a un entorno de desarrollo semi-interactivo de pruebas comprobadas. Las aplicaciones más habituales y típicas para este programa son, por ejemplo, la formalización de la semántica de los lenguajes de programación. En este punto, podemos nombrar el proyecto de certificación del compilador de CompCert o la certificación de Java Card EAL7, todo ello en el contexto industrial. Otro campo de aplicación muy claro es el de la formalización de las matemáticas    y su enseñanza.

Este programa nos permite expresar afirmaciones matemáticas, comprobaciones mecánicas de las mismas, así como también nos ayuda a encontrar pruebas formales de la certeza de las aseveraciones. Este programa trabaja dentro de la teoría del cálculo de construcciones inductivas, una derivación del cálculo de construcciones. Coq no es un comprobador automático de teoremas pero incluye tácticas automáticas de comprobación y varios procedimientos de decisión.