Convocatoria: Fondo Clemente Estable (FCE 20011)
Fuente de financiamiento: Agencia Nacional de Investigación e Innovación.
Duración: 20 meses.
Fecha de aprobación: noviembre de 2011
Fecha de comienzo: agosto de 2013
Fecha de finalización: marzo 2015
Palabras clave: Metateoría Formal, Programación con Tipos Dependientes
Resumen
El objetivo de este proyecto es estudiar distintos sistemas sintácticos de tratamiento de las variables ligadas, con el fin de llegar a resultados efectivos sobre la aplicabilidad de estos sistemas. Se utiliza para ello la Teoría Constructiva de Tipos como sistema lógico. Esto nos permite también investigar métodos de programación con tipos dependientes por medio de la experimentación con métodos de formalización que no han sido abordados previamente.