Master Class Coq

*(curso en francés, traducido simultáneamente al español)

El sistema Coq proporciona un lenguaje de programación simplificado para describir los algoritmos, las propiedades lógicas de estos algoritmos y las pruebas de que se cumplen las propiedades lógicas. La característica principal de este lenguaje es una versión extendida de la escritura como la que se encuentra en los lenguajes de programación convencionales. Aunque simplificado, este lenguaje es lo suficientemente poderoso para describir software avanzado, como una máquina virtual de Java, un compilador de C o un microprocesador.

Este curso utiliza el ejemplo de la base de datos para mostrar cómo aplicar Coq a las operaciones del modelo en los conjuntos de datos (intersección, unión, selección). Las propiedades lógicas ilustran cómo varias secuencias de operaciones pueden conducir al mismo resultado. Las técnicas de prueba se centran en los conectores lógicos básicos y en la técnica que permite razonar sobre conjuntos de tamaño ilimitado: la prueba recursiva. 

El curso también muestra cómo las diferentes opciones de estructura de datos permiten obtener programas más o menos eficientes, preservando la corrección de las operaciones realizadas. También se presentan técnicas para obtener código ejecutable a partir de modelos formales. Por último, el curso ofrece una visión general de las principales aplicaciones que se han desarrollado con el Coq y que sirven de base para proyectos cada vez más ambiciosos.

Yves Bertot es un director de investigación de Inria, especializado en pruebas de teoría de tipos, estudiando sucesivamente las propiedades de los lenguajes de programación, la geometría algorítmica, los cálculos matemáticos y la interacción entre la prueba formal y el cálculo formal algebraico.

Escribió junto con Pierre Castéran el primer libro sobre el sistema Coq que se publicó en 2004. Ha participado en algunos de los resultados más notables obtenidos con el sistema Coq, como el compilador CompCert y la prueba verificada por computadora del teorema de odd-order.