Compilación Certificada sobre Máquinas Abstractas de evaluación normal
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écnic...
| Main Author: | |
|---|---|
| Other Authors: | |
| Format: | doctoralThesis |
| Language: | spa |
| Published: |
2018
|
| Subjects: | |
| Online Access: | http://hdl.handle.net/11086/5801 |
| _version_ | 1801214250157342720 |
|---|---|
| author | Rodríguez, Leonardo Matías |
| author2 | Fridlender, Daniel Edgardo |
| author_facet | Fridlender, Daniel Edgardo Rodríguez, Leonardo Matías |
| author_sort | Rodríguez, Leonardo Matías |
| collection | Repositorio Digital Universitario |
| description | 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. |
| format | doctoralThesis |
| id | rdu-unc.5801 |
| institution | Universidad Nacional de Cordoba |
| language | spa |
| publishDate | 2018 |
| record_format | dspace |
| spelling | rdu-unc.58012022-10-13T11:16:44Z Compilación Certificada sobre Máquinas Abstractas de evaluación normal Rodríguez, Leonardo Matías Fridlender, Daniel Edgardo Especificación, verificación y razonamiento sobre programas Máquinas abstractas 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. 2018-02-05T19:40:10Z 2018-02-05T19:40:10Z 2017-03 doctoralThesis http://hdl.handle.net/11086/5801 spa Atribución 2.5 Argentina http://creativecommons.org/licenses/by/2.5/ar/ |
| spellingShingle | Especificación, verificación y razonamiento sobre programas Máquinas abstractas Rodríguez, Leonardo Matías Compilación Certificada sobre Máquinas Abstractas de evaluación normal |
| title | Compilación Certificada sobre Máquinas Abstractas de evaluación normal |
| title_full | Compilación Certificada sobre Máquinas Abstractas de evaluación normal |
| title_fullStr | Compilación Certificada sobre Máquinas Abstractas de evaluación normal |
| title_full_unstemmed | Compilación Certificada sobre Máquinas Abstractas de evaluación normal |
| title_short | Compilación Certificada sobre Máquinas Abstractas de evaluación normal |
| title_sort | compilacion certificada sobre maquinas abstractas de evaluacion normal |
| topic | Especificación, verificación y razonamiento sobre programas Máquinas abstractas |
| url | http://hdl.handle.net/11086/5801 |
| work_keys_str_mv | AT rodriguezleonardomatias compilacioncertificadasobremaquinasabstractasdeevaluacionnormal |