< Terug naar vorige pagina

Publicatie

StkTokens: Enforcing well-bracketed control flow and stack encapsulation using linear capabilities

Tijdschriftbijdrage - Tijdschriftartikel

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.

Tijdschrift: Journal of Functional Programming
ISSN: 0956-7968
Issue: e9
Volume: 31
Pagina's: 1-77
Jaar van publicatie:2021
BOF-keylabel:ja
IOF-keylabel:ja
BOF-publication weight:0.1
Auteurs:International
Authors from:Higher Education
Toegankelijkheid:Open