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.
Saved in:
| Main Authors: | , , |
|---|---|
| Format: | publishedVersion biblioteca |
| Language: | eng |
| Published: |
2016
|
| Subjects: | Compiler verification, Proof assistants, Biorthogonality, Step-indexed logical relations, |
| Online Access: | http://hdl.handle.net/11086/22139 https://doi.org/10.1016/j.entcs.2016.06.013 |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| id |
dig-unc-ar-11086-22139 |
|---|---|
| record_format |
koha |
| spelling |
dig-unc-ar-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 |
UNC AR |
| collection |
DSpace |
| country |
Argentina |
| countrycode |
AR |
| component |
Bibliográfico |
| access |
En linea |
| databasecode |
dig-unc-ar |
| tag |
biblioteca |
| region |
America del Sur |
| libraryname |
Biblioteca 'Ing. Agrónomo Moisés Farber' de la Facultad de Ciencias Agropecuarias |
| language |
eng |
| topic |
Compiler verification Proof assistants Biorthogonality Step-indexed logical relations Compiler verification Proof assistants Biorthogonality Step-indexed logical relations |
| spellingShingle |
Compiler verification Proof assistants Biorthogonality Step-indexed logical relations 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 |
| description |
Fil: Rodríguez, Leonardo. Universidad Nacional de Córdoba. Facultad de Matemática, Astronomía y Física; Argentina. |
| format |
publishedVersion |
| topic_facet |
Compiler verification Proof assistants Biorthogonality Step-indexed logical relations |
| 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 |
2016 |
| 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_ |
1787224638811537408 |