Blogs (1) >>
POPL 2019
Sun 13 - Sat 19 January 2019 Cascais, Portugal
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.66MiB

Wed 16 Jan

POPL-2019-Research-Papers
15:21 - 16:27: Research Papers - Capabilities and Session Types I at Sala II
Chair(s): Dominic OrchardUniversity of Kent, UK
POPL-2019-Research-Papers15:21 - 15:43
Talk
Lau SkorstengaardAarhus University, Dominique DevrieseVrije Universiteit Brussel, Belgium, Lars BirkedalAarhus University
Link to publication DOI Media Attached File Attached
POPL-2019-Research-Papers15:43 - 16:05
Talk
Simon CastellanImperial College London, UK, Nobuko YoshidaImperial College London
Link to publication DOI Pre-print Media Attached File Attached
POPL-2019-Research-Papers16:05 - 16:27
Talk
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