X-Git-Url: https://git.ralfj.de/web.git/blobdiff_plain/d60d764dc98f88b200c3b49525f413b5accdbe12..150148d32e74136bb0991ca60737a786feb2d344:/research/thesis.html?ds=sidebyside diff --git a/research/thesis.html b/research/thesis.html index 1ad155d..5efaad2 100644 --- a/research/thesis.html +++ b/research/thesis.html @@ -3,6 +3,11 @@ title: Understanding and Evolving the Rust Programming Language slug: Thesis --- +PhD Thesis, Defended in August 2020 + + +

Abstract

+

Rust is a young systems programming language that aims to fill the gap between high-level languages—which provide strong static guarantees like memory and thread safety—and low-level languages—which give the programmer fine-grained control over data layout and memory management. This dissertation presents two projects establishing the first formal foundations for Rust, enabling us to better understand and evolve this important language: RustBelt and Stacked Borrows.

RustBelt is a formal model of Rust’s type system, together with a soundness proof establishing memory and thread safety. The model is designed to verify the safety of a number of intricate APIs from the Rust standard library, despite the fact that the implementations of these APIs use unsafe language features.

@@ -11,10 +16,18 @@ slug: Thesis

RustBelt is built on top of Iris, a language-agnostic framework, implemented in the Coq proof assistant, for building higher-order concurrent separation logics. This dissertation begins by giving an introduction to Iris, and explaining how Iris enables the derivation of complex high-level reasoning principles from a few simple ingredients. In RustBelt, this technique is exploited crucially to introduce the lifetime logic, which provides a novel separation-logic account of borrowing, a key distinguishing feature of the Rust type system.

+

+This thesis has received an Honorable Mention for the ACM Doctoral Dissertation Award, +the ACM SIGPLAN John C. Reynolds Doctoral Dissertation Award (as one of two recipients), +an Otto Hahn Medal, +the ETAPS Doctoral Dissertation Award, +and the Saarland University Dr. Eduard Martin-Preis. +

+

Download and references