Convocatoria: Vinculación con científicos y tecnólogos uruguayos en el exterior (VCT 2008)
Investigador visitante: Dra. Maribel Fernández
Fuente de financiamiento: ANII
Duración: 15 días.
Fecha de aprobación: noviembre de 2008.
Fecha de comienzo: marzo de 2009.
Fecha de finalización: abril de 2009.
Palabras clave: Cálculo lambda, sintaxis nominal, teoría de tipos
Resumen
Esta propuesta se enmarca en 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.