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.

@article{paperbot1238,
  title = {StkTokens
                    <i>: Enforcing well-bracketed control flow and stack encapsulation using linear capabilities</i>},
  author = {LAU SKORSTENGAARD and DOMINIQUE DEVRIESE and LARS BIRKEDAL},
  journal = {Journal of Functional Programming},
  volume = {31},
  year = {2021},
  doi = {10.1017/s095679682100006x}
}