Fully abstract trace semantics for protected module architectures

DOI10.1016/j.cl.2015.03.002zbMath1387.68054OpenAlexW2079755135MaRDI QIDQ1749116

Dave Clarke, Marco Patrignani

Publication date: 15 May 2018

Published in: Computer Languages, Systems \& Structures (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/j.cl.2015.03.002

zbMATH Keywords

formal languagesfully abstract semanticstrace semanticsprotected modules architecturesuntyped assembly language

Mathematics Subject Classification ID

Theory of programming languages (68N15) Semantics in the theory of computing (68Q55)

Related Items (2)

Trace-Relating Compiler Correctness and Secure Compilation ⋮ Fully abstract trace semantics for protected module architectures

Uses Software

• Java Jr
• Sancus
• Fides
• TALx86

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• A fully abstract may testing semantics for concurrent objects
• LCF considered as a programming language
• Fully abstract models of typed \(\lambda\)-calculi
• Fully abstract trace semantics for protected module architectures
• Definability and Full Abstraction
• High-level separation logic for low-level code
• Biorthogonality, step-indexing and compiler correctness
• The marriage of bisimulations and Kripke logical relations
• A System-Level Game Semantics
• An equivalence-preserving CPS translation via multi-language semantics
• Programming Languages and Systems
• A kripke logical relation between ML and assembly
• Foundations of Software Science and Computational Structures

This page was built for publication: Fully abstract trace semantics for protected module architectures