This program is tentative and subject to change.
The Rust programming language continues to rise in popularity, and as such, warrants the close attention of the programming languages community. In this work, we present a new foundational contribution towards the theoretical understanding of Rust’s semantics. We prove that LLBC, a high-level, borrow-centric model previously proposed for Rust’s semantics and execution, is sound with regards to a low-level pointer-based language \emph{à la} CompCert. Specifically, we prove the following: that LLBC is a correct view over a traditional model of execution; that LLBC’s symbolic semantics are a correct abstraction of LLBC programs; and that LLBC’s symbolic semantics act as a borrow-checker for LLBC, i.e. that symbolically-checked LLBC programs do not get stuck when executed on a heap-and-addresses model of execution.
To prove these results, we introduce a new proof style that considerably simplifies our proofs of simulation, which relies on a notion of hybrid states. Equipped with this reasoning framework, we show that a new addition to LLBC’s symbolic semantics, namely a join operation, preserves the abstraction and borrow-checking properties. This in turn allows us to add support for loops to the Aeneas framework; we show, using a series of examples and case studies, that this unlocks new expressive power for Aeneas.
This program is tentative and subject to change.
Thu 5 SepDisplayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change
13:30 - 15:00 | Memory Models / Memory Management / Low-Level LanguagesICFP Papers and Events | ||
13:30 18mTalk | Oxidizing OCaml with Modal Memory Management ICFP Papers and Events Anton Lorenzen University of Edinburgh, Leo White Jane Street, Stephen Dolan Jane Street, Richard A. Eisenberg Jane Street, Sam Lindley University of Edinburgh DOI Pre-print | ||
13:48 18mTalk | A Two-Phase Infinite/Finite Low-Level Memory Model ICFP Papers and Events Calvin Beck University of Pennsylvania, Steve Zdancewic University of Pennsylvania, Irene Yoon INRIA Paris, Hanxi Chen University of Pennsylvania, Yannick Zakowski Inria | ||
14:06 18mTalk | Double-Ended Bit-Stealing for Algebraic Data Types ICFP Papers and Events Martin Elsman University of Copenhagen, Denmark Link to publication DOI | ||
14:24 18mTalk | Beyond Trees: Calculating Graph-Based Compilers ICFP Papers and Events Pre-print | ||
14:42 18mTalk | Sound Borrow-Checking for Rust via Symbolic Semantics ICFP Papers and Events |