X-Git-Url: https://git.ralfj.de/web.git/blobdiff_plain/1b67ebdd93edaf4a54bb1e4141074e9b5e647f6b..e950fd61d804302d1d40b61be7b576a140cf356c:/research/thesis.html diff --git a/research/thesis.html b/research/thesis.html index 1aaf050..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 + + +
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,6 +16,14 @@ slug: ThesisRustBelt 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. +
+