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