StkTokens: Enforcing well-bracketed control flow and stack encapsulation using linear capabilities

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

Mathematics Subject Classification ID

Functional programming and lambda calculus (68N18)

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