Proving correctness of a compiler using step-indexed logical relations

DOI10.1016/J.ENTCS.2016.06.013MaRDI QIDQ1744423zbMATH OpenOpenAlexWikidataFDO

Authors Leonardo Rodríguez, Miguel Pagano, Daniel Fridlender

Publication date 23 April 2018

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

zbMATH Keywords

proof assistantsbiorthogonalitycompiler verificationstep-indexed logical relations

Mathematics Subject Classification ID

Theory of compilers and interpreters (68N20) Functional programming and lambda calculus (68N18)

Recommendations

• Biorthogonality, step-indexing and compiler correctness
• Formal certification of a compiler back-end or: programming a compiler with a proof assistant
• scientific article; zbMATH DE number 2079040
• A Kripke logical relation between ML and assembly
• scientific article; zbMATH DE number 3898208

Cites work

• scientific article; zbMATH DE number 3485184 (Why is no real title available?)
• scientific article; zbMATH DE number 3291623 (Why is no real title available?)
• A call-by-name lambda-calculus machine
• A certified extension of the Krivine machine for a call-by-name higher-order imperative language
• A verified compiler for an impure functional language
• Biorthogonality, step-indexing and compiler correctness
• Classical logic, storage operators and second-order lambda-calculus
• Coinductive big-step operational semantics
• Deriving a lazy abstract machine
• Galois Connexions
• Implementing lazy functional languages on stock hardware: the Spineless Tagless G-machine
• Mechanized semantics
• Operational reasoning for functions with local state
• Programming Languages and Systems
• Separation Logic for Small-Step cminor
• The Mechanical Evaluation of Expressions
• The coherence of languages with intersection types
• The impact of higher-order state and control effects on local relational reasoning

Cited in

(6)

• scientific article; zbMATH DE number 1927430 (Why is no real title available?)
• Proving correctness of compilers using structured graphs
• A Kripke logical relation between ML and assembly
• A certified extension of the Krivine machine for a call-by-name higher-order imperative language
• Biorthogonality, step-indexing and compiler correctness
• scientific article; zbMATH DE number 2079040 (Why is no real title available?)

Describes a project that uses

Uses Software

• cminor
• Coq

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

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q1744423)