ANII | Agencia Nacional de Investigación e Innovación

El desarrollo de software de corrección certificada (cero falla) es imprescindible en aplicaciones complejas donde el error es inaceptable, como aplicaciones médicas, de telecomunicaciones, etc. Los sistemas de formalización de la demostración matemática (también llamados asistentes de prueba) son una herramienta esencial para la construcción de programas de corrección certificada. Utilizando estos asistentes pueden probarse propiedades de los lenguajes de programación o de programas (por ejemplo, corrección), principalmente por inducción sobre las estructuras del lenguaje objeto. Hay varios enfoques para la definición de asistentes de prueba utilizados en la verificación de software. El subyacente a esta propuesta tiene como punto de partida la utilización de un sistema formal basado en la Lógica Nominal, en el que se representan los lenguajes y programas sobre los que se quiere razonar. El enfoque nominal permite trabajar con nombres de variables, y las pruebas formales construidas en sintaxis nominal son similares a las pruebas construidas manualmente, lo que facilita su comprensión. La sintaxis nominal permite, entre otras cosas, razonar inductivamente sobre las clases de programas que difieren solo en los nombres elegidos para las variables, de la manera en que razonan informalmente los programadores. Para poder definir sistemas de prueba expresivos, la sintaxis nominal tiene que ser acompañada de un sistema de tipos dependiente y un mecanismo de evaluación. En este curso presentaremos los fundamentos teóricos de los sistemas de razonamiento nominal basados en reescritura y los sistemas de tipos existentes.