Proving correctness of a compiler using step-indexed logical relations

Fil: Rodríguez, Leonardo. Universidad Nacional de Córdoba. Facultad de Matemática, Astronomía y Física; Argentina.

Guardado en:
Detalles Bibliográficos
Autores principales: Rodríguez, Leonardo, Pagano, Miguel, Fridlender, Daniel
Formato: publishedVersion article
Lenguaje:Inglés
Publicado: 2021
Materias:
Compiler verification
Proof assistants
Biorthogonality
Step-indexed logical relations
Acceso en línea:http://hdl.handle.net/11086/22139
https://doi.org/10.1016/j.entcs.2016.06.013
Aporte de:
Repositorio Digital Universitario (UNC) de Universidad Nacional de Córdoba
id I10-R141-11086-22139
record_format dspace
spelling I10-R141-11086-221392023-11-08T16:52:14Z Proving correctness of a compiler using step-indexed logical relations Rodríguez, Leonardo Pagano, Miguel Fridlender, Daniel Compiler verification Proof assistants Biorthogonality Step-indexed logical relations publishedVersion publishedVersion Fil: Rodríguez, Leonardo. Universidad Nacional de Córdoba. Facultad de Matemática, Astronomía y Física; Argentina. Fil: Pagano, Miguel. Universidad Nacional de Córdoba. Facultad de Matemática, Astronomía y Física; Argentina. Fil: Fridlender, Daniel. Universidad Nacional de Córdoba. Facultad de Matemática, Astronomía y Física; Argentina. In this paper we prove the correctness of a compiler for a call-by-name language using step-indexed logical relations and biorthogonality. The source language is an extension of the simply typed lambda-calculus with recursion, and the target language is an extension of the Krivine abstract machine. We formalized the proof in the Coq proof assistant. https://www.sciencedirect.com/science/article/pii/S157106611630041X publishedVersion publishedVersion Fil: Rodríguez, Leonardo. Universidad Nacional de Córdoba. Facultad de Matemática, Astronomía y Física; Argentina. Fil: Pagano, Miguel. Universidad Nacional de Córdoba. Facultad de Matemática, Astronomía y Física; Argentina. Fil: Fridlender, Daniel. Universidad Nacional de Córdoba. Facultad de Matemática, Astronomía y Física; Argentina. Ciencias de la Computación 2021-12-29T20:38:31Z 2021-12-29T20:38:31Z 2016 article http://hdl.handle.net/11086/22139 https://doi.org/10.1016/j.entcs.2016.06.013 eng Attribution-NonCommercial-NoDerivatives 4.0 International http://creativecommons.org/licenses/by-nc-nd/4.0/ Impreso; Electrónico y/o Digital ISSN: 1571-0661
institution Universidad Nacional de Córdoba
institution_str I-10
repository_str R-141
collection Repositorio Digital Universitario (UNC)
language Inglés
topic Compiler verification
Proof assistants
Biorthogonality
Step-indexed logical relations
spellingShingle Compiler verification
Proof assistants
Biorthogonality
Step-indexed logical relations
Rodríguez, Leonardo
Pagano, Miguel
Fridlender, Daniel
Proving correctness of a compiler using step-indexed logical relations
topic_facet Compiler verification
Proof assistants
Biorthogonality
Step-indexed logical relations
description Fil: Rodríguez, Leonardo. Universidad Nacional de Córdoba. Facultad de Matemática, Astronomía y Física; Argentina.
format publishedVersion
publishedVersion
article
author Rodríguez, Leonardo
Pagano, Miguel
Fridlender, Daniel
author_facet Rodríguez, Leonardo
Pagano, Miguel
Fridlender, Daniel
author_sort Rodríguez, Leonardo
title Proving correctness of a compiler using step-indexed logical relations
title_short Proving correctness of a compiler using step-indexed logical relations
title_full Proving correctness of a compiler using step-indexed logical relations
title_fullStr Proving correctness of a compiler using step-indexed logical relations
title_full_unstemmed Proving correctness of a compiler using step-indexed logical relations
title_sort proving correctness of a compiler using step-indexed logical relations
publishDate 2021
url http://hdl.handle.net/11086/22139
https://doi.org/10.1016/j.entcs.2016.06.013
work_keys_str_mv AT rodriguezleonardo provingcorrectnessofacompilerusingstepindexedlogicalrelations
AT paganomiguel provingcorrectnessofacompilerusingstepindexedlogicalrelations
AT fridlenderdaniel provingcorrectnessofacompilerusingstepindexedlogicalrelations
_version_ 1806948613247467520

Ejemplares similares