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 |