Typed closure conversion preserves observational equivalence

DOI10.1145/1411204.1411227MaRDI QIDQ5178761zbMATH OpenOpenAlexDBLPWikidataFDO

Authors Amal Ahmed, Matthias Blume

Publication date 16 March 2015

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

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

zbMATH Keywords

full abstractionstep-indexed logical relationsequivalence-preserving compilationtyped closure conversion

Mathematics Subject Classification ID

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

Recommendations

• An equivalence-preserving CPS translation via multi-language semantics
• Fully abstract compilation via universal embedding
• Fully-abstract compilation by approximate back-translation
• Modular, fully-abstract compilation by approximate back-translation
• scientific article; zbMATH DE number 1231621

Cited in

(11)

• scientific article; zbMATH DE number 1497777 (Why is no real title available?)
• Fully Abstract and Robust Compilation
• An equivalence-preserving CPS translation via multi-language semantics
• Observational program calculi and the correctness of translations
• Modular, fully-abstract compilation by approximate back-translation
• Fully abstract compilation to JavaScript
• Fully abstract compilation via universal embedding
• scientific article; zbMATH DE number 7407781 (Why is no real title available?)
• Parametric Polymorphism — Universally
• Fully-abstract compilation by approximate back-translation
• Universal properties for universal types in bifibrational parametricity

This page was built for publication: Typed closure conversion preserves observational equivalence

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