Full Abstraction for Language Design (Short talk)
Full abstraction can be used to specify that a compilation process preserves equational reasoning on the source language – in other words, the semantics of the low-level target language does not leak into source programs.
Abstraction leaks are not only compiler and system security issues, but also usability issues. Multi-language programming systems are widely used, but often exhibit unfortunate, unplanned interactions. We use full abstraction for language design, to specify that the languages of a multi-language system interact gracefully – in a way that is also, in particular, amenable to secure compilation.
We demonstrate our approach by the case-study of a proposed multi-language design that combines a simple ML language with a linear language with linear mutable state. We prove that programmers knowing only the ML side of the story will not have bad surprises when interacting with other code that may, internally, use the linear language.
Sun 15 JanDisplayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change
10:30 - 12:00
|What is Secure Compilation? Part II (Short talk)|
Cătălin Hriţcu Inria ParisLink to publication
|Can relational logic facilitate secure compilation? (Short talk)|
David Naumann Stevens Institute of TechnologyFile Attached
|Full Abstraction for Language Design (Short talk)|
Gabriel Scherer Northeastern UniversityFile Attached
|Cogent: Where we Stand and What Comes Next (Short talk)|
Christine Rizkallah University of Pennsylvania, USAFile Attached
|Enforcing Well-Bracketed Control Flow on a Capability Machine using Local Capabilities|