Se ha lanzado la versión 8.12 (la última versión menor disponible en el momento de escribir esta noticia es la 8.12.1) de la herramienta interactiva de demostración de teoremas Coq (gallo).
Coq incluye el lenguaje de programación de tipo dependiente Gallina (pollo), que se basa en la teoría del cálculo de constructos.
El sistema Coq le permite desarrollar programas y pruebas de teoremas verificables por computadora junto con pruebas de conformidad con la especificación.
La nueva versión mejoró significativamente la biblioteca y la documentación estándar y también corrigió una serie de errores.
Fuente: linux.org.ru