An equivalence-preserving CPS translation via multi-language semantics

DOI10.1145/2034773.2034830MaRDI QIDQ5176993zbMATH OpenOpenAlexWikidataFDO

Authors Amal Ahmed, Matthias Blume

Publication date 5 March 2015

Published in Proceedings of the 16th ACM SIGPLAN international conference on Functional programming (Search for Journal in Brave)

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

zbMATH Keywords

back-translationcontinuation-passing styleequivalence-preserving compilationfull abstractionlogical relationsmulti-language semantics

Mathematics Subject Classification ID

Functional programming and lambda calculus (68N18) Theory of compilers and interpreters (68N20) Semantics in the theory of computing (68Q55) Specification and verification (program logics, model checking, etc.) (68Q60)

Recommendations

• Typed closure conversion preserves observational equivalence
• Fully abstract compilation via universal embedding
• Fully-abstract compilation by approximate back-translation
• Modular, fully-abstract compilation by approximate back-translation
• Verification, Model Checking, and Abstract Interpretation

Cited in

(14)

• CPS-translation as adjoint
• Fully abstract trace semantics for protected module architectures
• Equational logic and categorical semantics for multi-languages
• On multi-language abstraction. Towards a static analysis of multi-language programs
• Observational program calculi and the correctness of translations
• Fully-abstract compilation by approximate back-translation
• Fully abstract compilation via universal embedding
• Modular, fully-abstract compilation by approximate back-translation
• StkTokens: enforcing well-bracketed control flow and stack encapsulation using linear capabilities
• ANF preserves dependent types up to extensional equality
• Typed closure conversion preserves observational equivalence
• Fully Abstract and Robust Compilation
• On multi-language abstraction: towards a static analysis of multi-language programs
• On the semantic expressiveness of iso- and equi-recursive types

This page was built for publication: An equivalence-preserving CPS translation via multi-language semantics

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