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.
Original language | English |
---|---|
Article number | e9 |
Pages (from-to) | 1-77 |
Number of pages | 77 |
Journal | Journal of Functional Programming |
Volume | 31 |
Issue number | e9 |
DOIs | |
Publication status | Published - 15 Apr 2021 |