Sat 13 Jan 2018 11:00 - 11:30 at Hershey - Session 1 Chair(s): Amal Ahmed

We propose and study 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 new type of capabilities that are prevented by the hardware from being duplicated. In addition to designing and formalising this new calling convention, we also contribute a new way to formalise and prove that it effectively enforces well-bracketed control flow and local state encapsulation, building on the concept of fully abstract compilation.

Presentation (presentation.pdf)509KiB
Extended abstract (linear-well-bracketed-control.pdf)286KiB

Sat 13 Jan

10:30 - 11:30: PriSC 2018 - Session 1 at Hershey
Chair(s): Amal AhmedNortheastern University, USA
prisc-2018151583580000010:30 - 11:00
File Attached
prisc-2018151583760000011:00 - 11:30
File Attached