Fully abstract compilation via universal embedding

DOI10.1145/2951913.2951941MaRDI QIDQ2982006zbMATH OpenOpenAlexFDO

Authors Max New, William J. Bowman, Amal Ahmed

Publication date 10 May 2017

Published in Proceedings of the 21st ACM SIGPLAN International Conference on Functional Programming (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1145/2951913.2951941

zbMATH Keywords

back-translation polymorphismfully abstract compilationlogical relationsmulti-language semanticsparametricitysecure compilationuniversal domainuniversal embedding

Mathematics Subject Classification ID

Functional programming and lambda calculus (68N18) Theory of compilers and interpreters (68N20) Semantics in the theory of computing (68Q55)

Recommendations

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

Cited in

(17)

• A categorical approach to secure compilation
• Fully-abstract compilation by approximate back-translation
• Fully abstract compilation to JavaScript
• A secure compiler for ML modules
• Modular, fully-abstract compilation by approximate back-translation
• Linear capabilities for fully abstract compilation of separation-logic-verified code
• 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
• Logic Programming
• Robustly safe compilation
• Fully Abstract and Robust Compilation
• Logical predicates in higher-order mathematical operational semantics
• Bialgebraic reasoning on higher-order program equivalence
• On the semantic expressiveness of iso- and equi-recursive types
• Nanopass back-translation of call-return trees for mechanized secure compilation proofs

This page was built for publication: Fully abstract compilation via universal embedding

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