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.67MiB

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
Simon CastellanImperial College London, UK, Nobuko YoshidaImperial College London
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