Gadea, Alejandro Emilio, 1986-

Estudio de semántica categórica para lenguajes Algol-Like / Alejandro Emilio Gadea. - [S.l. : s.n. ], 2013. - iii, 77 páginas : ilustraciones ; 30 cm.

Tesis (Lic. en Ciencias de la Computación)--Universidad Nacional de Córdoba, Facultad de Matemática, Astronomía y Física, 2013.

Bibliografía: p. 77.

Cálculo lambda simplemente tipado -- Cálculo lambda tipado con subtipos -- Sintaxis de λlike -- Reglas de inferencia para λlike -- Semántica para λlike -- Implementación en Idris.


Este trabajo consiste en la definición y estudio de tres lenguajes de programación. Los dos primeros serán lenguajes funcionales, uno con un sistema de tipos simple y otro con un sistema de tipos que soporta subtipado. El tercero es un lenguaje funcional con aspectos imperativos, perteneciente a la clase de lenguajes Algol-Like. Para la definición semántica se utiliza teoría de categorías, en particular en la definición de los modelos semánticos. Siguiendo propuestas de Reynolds y Oles, utilizamos categorías funtoriales para el lenguaje Algol-like. Además se presentan las pruebas de ciertas propiedades deseables de las modelos semánticos dados: para el primer lenguaje nos enfocamos en la continuidad de las ecuaciones semánticas y en la corrección de la reducción;en el segundo lenguaje, desarrollamos la prueba de coherencia para diferentes derivaciones del mismo juicio; y para el tercero, probamos la naturalidad de las ecuaciones semánticas. El trabajo teórico estuvo acompañado de la implementación de evaluadores en Idris, un lenguaje con tipos dependientes.


Semantics of programming languages--Denotational semantics
Mathematical Logic --Lambda calculus and related systems

Stack discipline Semántica denotacional Categorías Categoría funtorial