Teoría de tipos dependientes: meta-teoría y aplicaciones

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.

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.