Proving correctness of a compiler using step-indexed logical relations

DOI10.1016/j.entcs.2016.06.013zbMath1401.68035OpenAlexW2474272294WikidataQ113317678 ScholiaQ113317678MaRDI QIDQ1744423

Daniel Fridlender, Miguel Pagano, Leonardo Rodríguez

Publication date: 23 April 2018

Full work available at URL: https://doi.org/10.1016/j.entcs.2016.06.013

zbMATH Keywords

biorthogonalityproof assistantscompiler verificationstep-indexed logical relations

Mathematics Subject Classification ID

Uses Software

• Coq
• cminor

Cites Work

• Coinductive big-step operational semantics
• Classical logic, storage operators and second-order lambda-calculus
• A call-by-name lambda-calculus machine
• Biorthogonality, step-indexing and compiler correctness
• Mechanized semantics
• Separation Logic for Small-Step cminor
• Implementing lazy functional languages on stock hardware: the Spineless Tagless G-machine
• Deriving a lazy abstract machine
• The coherence of languages with intersection types
• The impact of higher-order state and control effects on local relational reasoning
• A verified compiler for an impure functional language
• The Mechanical Evaluation of Expressions
• Galois Connexions
• Programming Languages and Systems
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item

This page was built for publication: Proving correctness of a compiler using step-indexed logical relations