Modular, fully-abstract compilation by approximate back-translation

DOI10.23638/LMCS-13(4:2)2017MaRDI QIDQ4596778zbMATH OpenFDO

Authors Dominique Devriese, Marco Patrignani, Frank Piessens, Steven Keuchel

Publication date 11 December 2017

Full work available at URL https://arxiv.org/abs/1703.09988

zbMATH Keywords

fully abstract compilation, cros-language logical relationmodular compilation

Mathematics Subject Classification ID

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

Recommendations

• Fully-abstract compilation by approximate back-translation
• Fully abstract compilation via universal embedding
• Fully abstract compilation to JavaScript
• Typed closure conversion preserves observational equivalence
• An equivalence-preserving CPS translation via multi-language semantics

Cited in

(13)

• A categorical approach to secure compilation
• Fully-abstract compilation by approximate back-translation
• Fully abstract compilation to JavaScript
• Fully abstract compilation via universal embedding
• A secure compiler for ML modules
• StkTokens: enforcing well-bracketed control flow and stack encapsulation using linear capabilities
• Trace-relating compiler correctness and secure compilation
• An equivalence-preserving CPS translation via multi-language semantics
• Typed closure conversion preserves observational equivalence
• Robustly safe compilation
• Fully Abstract and Robust Compilation
• On the semantic expressiveness of iso- and equi-recursive types
• Nanopass back-translation of call-return trees for mechanized secure compilation proofs

Describes a project that uses

Uses Software

• Coq

This page was built for publication: Modular, fully-abstract compilation by approximate back-translation

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