StkTokens : Enforcing well-bracketed control flow and stack encapsulation using linear capabilities
The work
| Authors | Lau Skorstengaard; Dominique Devriese; Lars Birkedal |
|---|---|
| Editors | |
| Type | article |
| Year | 2021 |
| Citekey | skorstengaard2021stktokens |
Where it appeared
| Published in | Journal of Functional Programming |
|---|---|
| Publisher | Cambridge University Press |
| Volume | 31 |
Identifiers
| DOI | 10.1017/s095679682100006x |
|---|---|
| OpenAlex | W3152835471 |
Access
| Landing page | https://doi.org/10.1017/s095679682100006x |
|---|
Related
| Distinct from | skorstengaard2019stktokens |
|---|
From OpenAlex, which stores abstracts as an index of words and their positions: what is shown is rebuilt from that, and reads fluently whether or not it is what the author wrote.
Abstract
Abstract We propose and study StkTokens: a new calling convention that provably enforces well-bracketed control flow and local state encapsulation on a capability machine. The calling convention is based on linear capabilities: a type of capabilities that are prevented from being duplicated by the hardware. In addition to designing and formalizing this new calling convention, we also contribute a new way to formalize and prove that it effectively enforces well-bracketed control flow and local state encapsulation using what we call a fully abstract overlay semantics.
How it got here
| How it got here | agent via openalex |
|---|---|
| Added | 2026-10-26 04:51 UTC |
| Not denied by | a person 2026-10-29 17:12 UTC |
Filed under
Cite it as
@article{skorstengaard2021stktokens,
title = {StkTokens : Enforcing well-bracketed control flow and stack encapsulation using linear capabilities},
author = {Lau Skorstengaard and Dominique Devriese and Lars Birkedal},
year = {2021},
journal = {Journal of Functional Programming},
publisher = {Cambridge University Press},
volume = {31},
doi = {10.1017/s095679682100006x},
}
This record lives at https://refs.drheap.org/skorstengaard2021stktokens/ and will keep doing so.