Coq
De Wikipedia, la enciclopedia libre
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 pruebas para esas aserciones y extrae programas certificados (correctos) a partir de las pruebas constructivas de aserciones que representan su especificación formal. Coq trabaja basándose en la teoría del Cálculo de Construcciones Inductivas, que es una teoría derivada del Cálculo de Construcciones.
Fue desarrollado en Francia, en le proyecto LogiCal, entre el INRIA, la École Polytechnique, la Universidad París XI y el CNRS. Dirigen el desarrollo los investigadores Gilles Dowek y Christine Paulin-Mohring. Coq está escrito en el lenguaje Ocaml.
[editar] Enlaces externos
El contenido de esta página es un esbozo sobre software. Ampliándolo ayudarás a mejorar Wikipedia.
Puedes ayudarte con las wikipedias en otras lenguas.
