Browsing by Author "Pagano, Miguel María"
Now showing items 1-7 of 7
-
Automatización para el entorno Isabelle / ZF
Steinberg, Matías Uriel (2021-03)Al formalizar en Isabelle/ZF las definiciones asociadas a Forcing para demostrar la independencia de la Hipótesis del Continuo, se presenta una cantidad significativa de tareas sistemáticas y repetitivas, entre las que se ... -
Biortogonalidad para corrección de compiladores y adecuación computacional
Gadea, Alejandro Emilio (2019)En esta tesis hemos estudiado en profundidad los métodos de biortogonalidad y step-indexing para probar tanto adecuación computacional como corrección de compiladores. Un primer aporte es la prueba de corrección de una ... -
A certified extension of the Krivine machine for a call-by-name higher-order imperative language
Rodríguez, Leonardo Matías; Fridlender, Daniel Edgardo; Pagano, Miguel María (2014)In this paper we present a compiler that translates programs from an imperative higher-order language into a sequence of instructions for an abstract machine. We consider an extension of the Krivine machine for the ... -
Formalización de fundaciones de la matemática y compiladores correctos por construcción
Gunther, Emmanuel (2019)Dentro de las teorías fundacionales de la matemática se encuentran la Teoría de Conjuntos y la Teoría de Tipos. La primera es bien conocida en la comunidad matemática; la teoría de tipos además de ser una posible fundación, ... -
Generación de código intermedio usando semántica funtorial
Rodríguez, Leonardo Matías (2010-12-29)Este trabajo consiste en la implementación de un front-end para un lenguaje de programación Algol-like. El front-end es la primera etapa del proceso de compilación; cuyo objetivo es generar código en un lenguaje intermedio ... -
Representación semántica de lenguaje natural en el dominio de fórmulas lógicas
Piloni, Diego (2018)Este trabajo final de licenciatura parte del supuesto que el aprendizaje del lenguaje simbólico de lógica formal es problemático (Oller, 2006). Algunos aspectos de esta dificultad son analizados por los autores de “Language, ... -
Soporte para ARM en un compilador verificado
Arranz Olmos, Santiago (2022-12)Este trabajo es un estudio de un lenguaje de programación, llamado Jasmin, utilizado para desarrollar criptografía eficiente y confiable, así como una propuesta de una extensión a esta herramienta para agregar soporte para ...