StkTokens: Enforcing well-bracketed control flow and stack encapsulation using linear capabilities
From MaRDI portal
Publication:5016212
DOI10.1017/S095679682100006XOpenAlexW3152835471MaRDI QIDQ5016212
Lau Skorstengaard, Dominique Devriese, Lars Birkedal
Publication date: 13 December 2021
Published in: Journal of Functional Programming (Search for Journal in Brave)
Full work available at URL: https://arxiv.org/abs/1811.02787
Related Items (2)
Linear capabilities for fully abstract compilation of separation-logic-verified code ⋮ StkTokens: Enforcing well-bracketed control flow and stack encapsulation using linear capabilities
Cites Work
- Unnamed Item
- Solving reflexive domain equations in a category of complete metric spaces
- Game semantics and linear CPS interpretation
- Reasoning about a machine with local capabilities. Provably safe stack and return pointer management
- Fully-abstract compilation by approximate back-translation
- Fully abstract compilation via universal embedding
- Data Types as Lattices
- 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
- StkTokens: Enforcing well-bracketed control flow and stack encapsulation using linear capabilities
- An equivalence-preserving CPS translation via multi-language semantics
- A kripke logical relation for effect-based program transformations
- A verified information-flow architecture
- Step-indexed kripke models over recursive worlds
- Programming semantics for multiprogrammed computations
This page was built for publication: StkTokens: Enforcing well-bracketed control flow and stack encapsulation using linear capabilities
