Proving compiler correctness using step-indexed logical relations

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....

Descripción completa

Guardado en:
Detalles Bibliográficos
Autores principales: Rodríguez, Leonardo, Pagano, Miguel, Fridlender, Daniel
Formato: 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-R14111086-22139
record_format dspace
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 compiler correctness using step-indexed logical relations
topic_facet Compiler verification
Proof assistants
Biorthogonality
Step-indexed logical relations
description 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.
format 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 compiler correctness using step-indexed logical relations
title_short Proving compiler correctness using step-indexed logical relations
title_full Proving compiler correctness using step-indexed logical relations
title_fullStr Proving compiler correctness using step-indexed logical relations
title_full_unstemmed Proving compiler correctness using step-indexed logical relations
title_sort proving compiler correctness 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 provingcompilercorrectnessusingstepindexedlogicalrelations
AT paganomiguel provingcompilercorrectnessusingstepindexedlogicalrelations
AT fridlenderdaniel provingcompilercorrectnessusingstepindexedlogicalrelations
bdutipo_str Repositorios
_version_ 1764820395286855682

Ejemplares similares