Compilación Certificada sobre Máquinas Abstractas de evaluación normal

Mostrar todas las versiones(2)

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...

Descripción completa

Guardado en:
Detalles Bibliográficos
Autor principal: Rodríguez, Leonardo Matías
Otros Autores: Fridlender, Daniel Edgardo
Formato: doctoralThesis
Lenguaje:Español
Publicado: 2018
Materias:
Especificación, verificación y razonamiento sobre programas
Máquinas abstractas
Acceso en línea:http://hdl.handle.net/11086/5801
Aporte de:
Repositorio Digital Universitario (UNC) de Universidad Nacional de Córdoba
id I10-R14111086-5801
record_format dspace
institution Universidad Nacional de Córdoba
institution_str I-10
repository_str R-141
collection Repositorio Digital Universitario (UNC)
language Español
topic Especificación, verificación y razonamiento sobre programas
Máquinas abstractas
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
topic_facet Especificación, verificación y razonamiento sobre programas
Máquinas abstractas
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.
author2 Fridlender, Daniel Edgardo
author_facet Fridlender, Daniel Edgardo
Rodríguez, Leonardo Matías
format doctoralThesis
author Rodríguez, Leonardo Matías
author_sort Rodríguez, Leonardo Matías
title 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_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_sort compilación certificada sobre máquinas abstractas de evaluación normal
publishDate 2018
url http://hdl.handle.net/11086/5801
work_keys_str_mv AT rodriguezleonardomatias compilacioncertificadasobremaquinasabstractasdeevaluacionnormal
bdutipo_str Repositorios
_version_ 1764820396384714752

Ejemplares similares