Fully Abstract and Robust Compilation

DOI10.1007/978-3-030-89051-3_6MaRDI QIDQ6488145zbMATH OpenFDO

Authors Carmine Abate, Matteo Busi, Stelios Tsampas

Publication date 29 March 2023

Full work available at URL https://doi.org/10.1007/978-3-030-89051-3_6

Mathematics Subject Classification ID

Theory of compilers and interpreters (68N20) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Semantics in the theory of computing (68Q55)

Recommendations

• Fully abstract compilation via universal embedding
• Modular, fully-abstract compilation by approximate back-translation
• Fully-abstract compilation by approximate back-translation
• Fully abstract compilation to JavaScript
• Typed closure conversion preserves observational equivalence

Cites work

• scientific article; zbMATH DE number 4008457 (Why is no real title available?)
• scientific article; zbMATH DE number 3485184 (Why is no real title available?)
• scientific article; zbMATH DE number 1086715 (Why is no real title available?)
• A categorical approach to secure compilation
• A verified CompCert front-end for a memory model supporting pointer arithmetic and uninitialised data
• An equivalence-preserving CPS translation via multi-language semantics
• Bialgebras for structural operational semantics: an introduction
• Compositional CompCert
• Determinacy \(\to\) (observation equivalence \(=\) trace equivalence)
• Formal certification of a compiler back-end or: programming a compiler with a proof assistant
• Full abstraction for expressiveness: history, myths and facts
• Fully abstract trace semantics for protected module architectures
• Fully-abstract compilation by approximate back-translation
• General conditions for full abstraction
• LCF considered as a programming language
• Noninterference for free
• On abstraction and the expressive power of programming languages
• Semantics with applications: an appetizer.
• Structural Operational Semantics for Stochastic Process Calculi
• Structural operational semantics.
• The verified CakeML compiler backend
• Towards Effects in Mathematical Operational Semantics
• Trace-relating compiler correctness and secure compilation
• Typed closure conversion preserves observational equivalence
• Well-behaved translations between structural operational semantics

Cited in

(3)

• Bialgebraic reasoning on higher-order program equivalence
• Robustly safe compilation
• Trace-relating compiler correctness and secure compilation

This page was built for publication: Fully Abstract and Robust Compilation

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