Fully-abstract compilation by approximate back-translation

DOI10.1145/2837614.2837618MaRDI QIDQ2828252zbMATH OpenOpenAlexWikidataFDO

Authors Dominique Devriese, Marco Patrignani, Frank Piessens

Publication date 24 October 2016

Published in Proceedings of the 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (Search for Journal in Brave)

Full work available at URL https://lirias.kuleuven.be/handle/123456789/570054

zbMATH Keywords

logical relationsstep-indexed logical relationssecure compilationcompiler securitycross-language logical relationsfully-abstract compilation

Mathematics Subject Classification ID

Theory of compilers and interpreters (68N20) Combinatory logic and lambda calculus (03B40) Logic in computer science (03B70)

Recommendations

• Modular, 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

(10)

• Linear capabilities for fully abstract compilation of separation-logic-verified code
• Fully abstract compilation to JavaScript
• Modular, fully-abstract compilation by approximate back-translation
• Robustly safe compilation
• An equivalence-preserving CPS translation via multi-language semantics
• Fully abstract compilation via universal embedding
• Fully Abstract and Robust Compilation
• Typed closure conversion preserves observational equivalence
• Trace-relating compiler correctness and secure compilation
• StkTokens: enforcing well-bracketed control flow and stack encapsulation using linear capabilities

This page was built for publication: 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 Q2828252)