POPL 2019 (series) / Research Papers /
StkTokens: Enforcing Well-Bracketed Control Flow and Stack Encapsulation Using Linear Capabilities
Wed 16 Jan 2019 15:21 - 15:43 at Sala II - Capabilities and Session Types I Chair(s): Dominic Orchard
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.
Presentation (presentation.pdf) | 9.67MiB |
Wed 16 Jan Times are displayed in time zone: Greenwich Mean Time : Belfast change
Wed 16 Jan
Times are displayed in time zone: Greenwich Mean Time : Belfast change
15:21 - 16:27: Capabilities and Session Types IResearch Papers at Sala II Chair(s): Dominic OrchardUniversity of Kent, UK | |||
15:21 - 15:43 Talk | StkTokens: Enforcing Well-Bracketed Control Flow and Stack Encapsulation Using Linear Capabilities Research Papers Lau SkorstengaardAarhus University, Dominique DevrieseVrije Universiteit Brussel, Belgium, Lars BirkedalAarhus University Link to publication DOI Media Attached File Attached | ||
15:43 - 16:05 Talk | Two sides of the same coin: Session Types and Game Semantics Research Papers Link to publication DOI Pre-print Media Attached File Attached | ||
16:05 - 16:27 Talk | Exceptional Asynchronous Session Types: Session Types without Tiers Research Papers Simon FowlerThe University of Edinburgh, Sam LindleyUniversity of Edinburgh, UK, J. Garrett MorrisUniversity of Kansas, USA, Sara Décova Link to publication DOI Pre-print Media Attached File Attached |