Informe final del proyecto: Control de tipos para Teoría de tipos nominal

Abstract

El objetivo estratégico de esta línea de investigación es la formulación e implementación de un un Nominal Logical Framework basado en la teoría de sintaxis abstracta nominal con tipos dependientes. Esto incluye el diseño e implementación del sistema formal y de un algoritmo de controlador de tipos que garantice la buena formación de expresiones de los sistemas representados. Se desarrollaron casos de representación de sistemas lógicos, incluyendo la Aritmética de Primer Orden y Lógica de Orden Superior, con el estudio correspondiente de la adecuación de cada representación. Se compararon estos resultados con los logrados por otros medios, tales como las Estructuras de Sistemas Lógicos (Logical Frameworks) basados en el Cálculo Lambda con tipos dependientes.