Proving compiler correctness using step-indexed logical relations

dc.creatorRodríguez, Leonardo
dc.creatorPagano, Miguel
dc.creatorFridlender, Daniel
dc.date.accessioned2021-12-29T20:38:31Z
dc.date.accessioned2022-10-14T18:31:58Z
dc.date.available2021-12-29T20:38:31Z
dc.date.available2022-10-14T18:31:58Z
dc.date.created2021-12-29T20:38:31Z
dc.date.issued2016
dc.identifierhttp://hdl.handle.net/11086/22139
dc.identifierhttps://doi.org/10.1016/j.entcs.2016.06.013
dc.identifier.urihttps://repositorioslatinoamericanos.uchile.cl/handle/2250/4274066
dc.description.abstractIn 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.
dc.languageeng
dc.rightshttp://creativecommons.org/licenses/by-nc-nd/4.0/
dc.rightsAttribution-NonCommercial-NoDerivatives 4.0 International
dc.sourceISSN: 1571-0661
dc.subjectCompiler verification
dc.subjectProof assistants
dc.subjectBiorthogonality
dc.subjectStep-indexed logical relations
dc.titleProving compiler correctness using step-indexed logical relations
dc.typearticle


Este ítem pertenece a la siguiente institución