CATÁLOGO DE LA BIBLIOTECA DE LA FaMAF
Normal view MARC view ISBD view

Compilación Certificada sobre Máquinas Abstractas de evaluación normal / Leonardo M. Rodríguez.

By: Rodríguez, Leonardo Matías, 1987-.
Contributor(s): Fridlender, Daniel Edgardo, 1964- [dir.].
Material type: materialTypeLabelBookPublisher: [S.l. : s.n. ], 2017Description: 169 p. : il.; 30 cm.Subject(s): Specifying , verifying and reasoning about programs | Especificación, verificación y razonamiento sobre programas | Compilación | Certificación | Semántica | Relaciones lógicas | Máquinas abstractas | RealizabilidadOnline resources: Acceso a Versión Digital | RDU-UNC Disponible en línea.Dissertation note: Tesis (Doctor en Ciencias de la Computación)--Universidad Nacional de Córdoba, Facultad de Matemática, Astronomía, Física y Computación, 2017. Summary: En esta tesis se analiza cómo demostrar la corrección de compiladores de lenguajes con evaluación normal, utilizando máquinas abstractas como entornos de ejecución. En particular se presenta una prueba de corrección de un compilador basada en la semántica denotacional del lenguaje, utilizando técnicas como step-indexing y biortogonalidad para definir relaciones lógicas que capturen la noción de corrección del compilador de manera composicional. Además, se desarrolla un enfoque basado en la noción de realizabilidad para demostrar la corrección del compilador en un lenguaje con evaluación lazy. Todas las pruebas de corrección presentadas en la tesis están formalizadas en Coq, un asistente de demostración con tipos dependientes.Summary: In this work we explore how to prove the correctness of compilers for call-by-name languages using abstract machines as runtime environments. We present a proof of correctness with respect to the denotational semantics of the source language, using methods as step-indexing and biorthogonality to define logical relations in order to capture a notion of correctness in a compositional manner. We also present an approach based on logical realizability to prove the correctness of a call-by-need language. Every proof as been formalized in Coq, a proof assistant with dependent types.
Tags from this library: No tags from this library for this title.
Item type Current location Call number URL Copy number Status Notes Date due Barcode Item holds
Tesis de Doctorado Tesis de Doctorado FaMAF
Vitrina
T C ROD http://www.famaf.unc.edu.ar/institucional/biblioteca/trabajos/639/18114.pdf 1 Available Disponible también en línea 22867
Total holds: 0

Bajo una Licencia Creative Commons Atribución 2.5 Argentina.

Incluye apéndices.

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

En esta tesis se analiza cómo demostrar la corrección de compiladores de lenguajes con evaluación normal, utilizando máquinas abstractas como entornos de ejecución. En particular se presenta una prueba de corrección de un compilador basada en la semántica denotacional del lenguaje, utilizando técnicas como step-indexing y biortogonalidad para definir relaciones lógicas que capturen la noción de corrección del compilador de manera composicional. Además, se desarrolla un enfoque basado en la noción de realizabilidad para demostrar la corrección del compilador en un lenguaje con evaluación lazy. Todas las pruebas de corrección presentadas en la tesis están formalizadas en Coq, un asistente de demostración con tipos dependientes.

In this work we explore how to prove the correctness of compilers for call-by-name languages using abstract machines as runtime environments. We present a proof of correctness with respect to the denotational semantics of the source language, using methods as step-indexing and biorthogonality to define logical relations in order to capture a notion of correctness in a compositional manner. We also present an approach based on logical realizability to prove the correctness of a call-by-need language. Every proof as been formalized in Coq, a proof assistant with dependent types.

Disponible en línea.

La biblioteca posee 1 ej.

Defensa: marzo 2017.

Click on an image to view it in the image viewer

Horario de la Biblioteca: lunes a viernes de 8:30 a 18:00hs

Av. Medina Allende s/n , Ciudad Universitaria, Córdoba, Argentina

Tel: +54 351 5353701 int. 41127(Atención al Público) int. 41151(Dirección)

biblio@famaf.unc.edu.ar

publicofamaf@gmail.com



//