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....
Guardado en:
| Autores principales: | , , |
|---|---|
| Formato: | article |
| Lenguaje: | Inglés |
| Publicado: |
2021
|
| Materias: | |
| Acceso en línea: | http://hdl.handle.net/11086/22139 https://doi.org/10.1016/j.entcs.2016.06.013 |
| Aporte de: |
| Sumario: | 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. |
|---|