Dependent Types for Nominal Terms

 

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.

Investigación

La Facultad de Ingeniería da servicios de apoyo a estudiantes avanzados y graduados para facilitar su inserción laboral. Según el último relevamiento realizado la facultad cuenta con plena inserción de sus graduados.

A través de este espacio se busca promover y dar a conocer las oportunidades que tienen las mujeres dentro del área de las Tecnologías de la Información y la Comunicación. Asimismo, se realizan diferentes actividades para impulsar a estudiar tecnología.

El Centro de Innovación y Emprendimientos (CIE) de la Universidad ORT Uruguay, promueve y desarrolla la generación de nuevos emprendedores. Sus acciones están dirigidas a fomentar la innovación, la actitud emprendedora y promover oportunidades.