Catálogo de publicaciones - tesis

Compartir en
redes sociales

Título de Acceso Abierto

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

Leonardo Matías Rodríguez Daniel Edgardo Fridlender

acceptedVersion.

Resumen/Descripción – provisto por el repositorio digital
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.
Palabras clave – provistas por el repositorio digital

Especificación, verificación y razonamiento sobre programas; Máquinas abstractas

Disponibilidad
Institución detectada Año de publicación Navegá Descargá Solicitá
No requiere 2017 Repositorio Digital Universitario (SNRD) acceso abierto

Información

Tipo de recurso:

tesis

Idiomas de la publicación

  • español castellano

País de edición

Argentina

Fecha de publicación