Master Class - "Coq, sistema de gestión de pruebas formales"

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

¿Qué descubriré en esta master class? 

En esta master class utilizaremos 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 diferentes 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.

Director de investigación en Inria, Yves Bertot se especializa en pruebas teórico-tipológicas, estudiando sucesivamente las propiedades de los lenguajes de programación, la geometría algorítmica, los cálculos matemáticos y las interacciones entre las pruebas formales y los cálculos algebraicos formales. Es coautor con Pierre Castéran del primer libro sobre el sistema Coq, “Interactive Theorem Proving And Program Development, Coq'art: The Calculus Of Inductive Constructions", publicado en 2004. Ha contribuido a algunos de los resultados más notables obtenidos con el sistema Coq, como el compilador CompCert y la prueba informática del teorema del orden impar.