Fully Abstract and Robust Compilation

DOI10.1007/978-3-030-89051-3_6zbMath1520.68025MaRDI QIDQ6488145

Carmine Abate, Stelios Tsampas, Matteo Busi

Publication date: 29 March 2023

Mathematics Subject Classification ID

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

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Bialgebras for structural operational semantics: an introduction
• Semantics with applications: an appetizer.
• Determinacy \(\to\) (observation equivalence \(=\) trace equivalence)
• LCF considered as a programming language
• On abstraction and the expressive power of programming languages
• A verified CompCert front-end for a memory model supporting pointer arithmetic and uninitialised data
• Fully abstract trace semantics for protected module architectures
• A categorical approach to secure compilation
• Compositional CompCert
• Fully-abstract compilation by approximate back-translation
• Well-behaved Translations between Structural Operational Semantics
• Noninterference for free
• The verified CakeML compiler backend
• Trace-Relating Compiler Correctness and Secure Compilation
• An equivalence-preserving CPS translation via multi-language semantics
• Typed closure conversion preserves observational equivalence
• Formal certification of a compiler back-end or
• Structural Operational Semantics for Stochastic Process Calculi
• Towards Effects in Mathematical Operational Semantics
• Full abstraction for expressiveness: history, myths and facts
• General conditions for full abstraction

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