StkTokens: enforcing well-bracketed control flow and stack encapsulation using linear capabilities
From MaRDI portal
Recommendations
- Reasoning about a machine with local capabilities. Provably safe stack and return pointer management
- Constraining Delimited Control with Contracts
- scientific article; zbMATH DE number 1956543
- Staged allocation: a compositional technique for specifying and implementing procedure calling conventions
- Stack-based typed assembly language
Cites work
- A Kripke logical relation for effect-based program transformations
- A verified information-flow architecture
- An equivalence-preserving CPS translation via multi-language semantics
- Data Types as Lattices
- Fully abstract compilation via universal embedding
- Fully-abstract compilation by approximate back-translation
- Game semantics and linear CPS interpretation
- Iris from the ground up: a modular foundation for higher-order concurrent separation logic
- Linear capabilities for fully abstract compilation of separation-logic-verified code
- Modular, fully-abstract compilation by approximate back-translation
- Programming semantics for multiprogrammed computations
- Reasoning about a machine with local capabilities. Provably safe stack and return pointer management
- Solving reflexive domain equations in a category of complete metric spaces
- Step-indexed Kripke models over recursive worlds
- StkTokens: enforcing well-bracketed control flow and stack encapsulation using linear capabilities
Cited in
(3)
This page was built for publication: StkTokens: enforcing well-bracketed control flow and stack encapsulation using linear capabilities
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5016212)
