Convocatoria: International Joint Projects
Fuente de Financiamiento: The Royal Society, UK
Duración: 24 meses
Fecha de Aprobación: Febrero/2009
Fecha de Comienzo: 06/2009
Fecha de Finalización: 06/2011
Palabras clave: Nominal Syntax, Lambda Calculus, Type Theory
Resumen
Esta propuesta se enmarca la teoría de sistemas lógicos o sistemas formales de formalización de la demostración matemática. La principal aplicación en informática de estos sistemas es en el desarrollo de software de corrección certificada (cero falla), imprescindible en aplicaciones complejas donde el error es inaceptable, como aplicaciones médicas, de telecomunicaciones, etc.
Hay varios enfoques en la aplicación de sistemas lógicos a la verificación de software; el subyacente a esta propuesta tiene como punto de partida la utilización de un sistema formal suficientemente expresivo como estructura de soporte (framework), en el que se representan los lenguajes objeto sobre los que se quiere razonar.
El sistema de base se implementa en máquina como un asistente en el desarrollo de las construcciones formales. Utilizando estos asistentes pueden introducirse los lenguajes objeto y probar propiedades de los programas utilizando principalmente inducción sobre las estructuras del lenguaje objeto.
Los sistemas de soporte que definen el estado del arte en esta área están basados en el calculo lambda, y representan los programas sobre los cuales se quiere razonar usando sintaxis de orden superior o representaciones concretas basadas en manipulación de índices.
Ambas alternativas presentan inconvenientes; en este proyecto proponemos utilizar la sintaxis nominal, que 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 desarrollar una teoría de tipos con sintaxis nominal que pueda ser usada como un sistema de soporte para lógicas en el sentido explicado, es necesario al menos desarrollar un sistema de tipos dependientes.
Esta visita establecerá las bases para una colaboración entre las dos instituciones con el objetivo de desarrollar un sistema de tipos dependientes con sintaxis nominal, y como primer paso al desarrollo de una teoría de tipos nominal.