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.
Main Authors: | , , |
---|---|
Format: | publishedVersion |
Language: | eng |
Published: |
2021
|
Subjects: | |
Online Access: | http://hdl.handle.net/11086/22139 https://doi.org/10.1016/j.entcs.2016.06.013 |
_version_ | 1801212508894134272 |
---|---|
author | Rodríguez, Leonardo Pagano, Miguel Fridlender, Daniel |
author_facet | Rodríguez, Leonardo Pagano, Miguel Fridlender, Daniel |
author_sort | Rodríguez, Leonardo |
collection | Repositorio Digital Universitario |
description | Fil: Rodríguez, Leonardo. Universidad Nacional de Córdoba. Facultad de Matemática, Astronomía y Física; Argentina. |
format | publishedVersion |
id | rdu-unc.22139 |
institution | Universidad Nacional de Cordoba |
language | eng |
publishDate | 2021 |
record_format | dspace |
spelling | rdu-unc.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 |
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 |
title | 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_short | Proving correctness of a compiler using
step-indexed logical relations |
title_sort | proving correctness of a compiler using step indexed logical relations |
topic | Compiler verification Proof assistants Biorthogonality Step-indexed logical relations |
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 |