Convocatoria: Proyectos de Movilidad - Cooperación con Argentina
Fuente de financiamiento: Agencia Nacional de Investigación e Innovación.
Duración: 24 meses.
Fecha de aprobación: Marzo 2015
Fecha de comienzo: Diciembre 2015
Fecha de finalización: Diciembre 2017
Resumen
En este proyecto se propone la investigación sobre Teorías de Tipos Dependientes en dos aspectos: como objeto de estudio en sí mismo, y su uso para la formalización de resultados meta-matemáticos de lenguajes de programación y de semántica formal de lenguajes naturales.
En el primer aspecto, nos proponemos obtener demostraciones formales en Teoría Constructiva de Tipos de resultados sintácticos clásicos del Cálculo Lambda y su generalización a sistemas de lenguajes con ligadura y reescritura, que servirán como base para el diseño y prototipación de un lenguaje de Teoría Constructiva de Tipos con tipos de registros dependientes, tipos inductivos y coinductivos y control de tipos basado en normalización por evaluación.
En el segundo aspecto, estudiaremos la utilización de sistemas de tipos para establecer propiedades de lógicas de alto orden utilizadas en el modelado de la semántica formal del lenguaje natural.