Show simple item record

Proving correctness of a compiler using step-indexed logical relations

dc.contributor.authorRodríguez, Leonardo
dc.contributor.authorPagano, Miguel
dc.contributor.authorFridlender, Daniel
dc.date.accessioned2021-12-29T20:38:31Z
dc.date.available2021-12-29T20:38:31Z
dc.date.issued2016
dc.identifier.urihttp://hdl.handle.net/11086/22139
dc.identifier.urihttps://doi.org/10.1016/j.entcs.2016.06.013
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.es
dc.description.urihttps://www.sciencedirect.com/science/article/pii/S157106611630041X
dc.format.mediumImpreso; Electrónico y/o Digital
dc.language.isoenges
dc.rightsAttribution-NonCommercial-NoDerivatives 4.0 International*
dc.rights.urihttp://creativecommons.org/licenses/by-nc-nd/4.0/*
dc.sourceISSN: 1571-0661
dc.subjectCompiler verificationen
dc.subjectProof assistantsen
dc.subjectBiorthogonalityen
dc.subjectStep-indexed logical relationsen
dc.titleProving correctness of a compiler using step-indexed logical relationsen
dc.typearticlees
dc.description.versionpublishedVersiones
dc.description.versionpublishedVersion
dc.description.filFil: Rodríguez, Leonardo. Universidad Nacional de Córdoba. Facultad de Matemática, Astronomía y Física; Argentina.es
dc.description.filFil: Pagano, Miguel. Universidad Nacional de Córdoba. Facultad de Matemática, Astronomía y Física; Argentina.es
dc.description.filFil: Fridlender, Daniel. Universidad Nacional de Córdoba. Facultad de Matemática, Astronomía y Física; Argentina.es
dc.journal.editorialElsevieres
dc.journal.pagination197-214es
dc.journal.titleElectronic Notes in Theoretical Computer Sciencees
dc.journal.volume323es
dc.description.fieldCiencias de la Computación
dc.conference.cityUnited States
dc.conference.countryBrasil
dc.conference.editorialElsevier
dc.conference.eventProceedings of the Tenth Workshop on Logical and Semantic Frameworks, with Applications (LSFA 2015)
dc.conference.eventcityNatak
dc.conference.eventcountryBrasil
dc.conference.eventdate2015-8
dc.conference.journalElectronic Notes in Theoretical Computer Science
dc.conference.publicationLibro
dc.conference.workArtículo Completo
dc.conference.typeWorkshop


Files in this item

Thumbnail
Name:
paper_.pdf
Size:
245.5Kb
Format:
PDF
View/Open

This item appears in the following Collection(s)

Show simple item record

Attribution-NonCommercial-NoDerivatives 4.0 International
Except where otherwise noted, this item's license is described as Attribution-NonCommercial-NoDerivatives 4.0 International