From: Ralf Jung Date: Thu, 16 Sep 2021 19:18:07 +0000 (-0400) Subject: be less redundant about the year of my thesis X-Git-Url: https://git.ralfj.de/web.git/commitdiff_plain/a2412af828fa3d5c8602bb47781f04913814e109 be less redundant about the year of my thesis --- diff --git a/research/thesis.html b/research/thesis.html index 082f9c1..b494077 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.

@@ -12,10 +17,10 @@ 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 2020 ACM Doctoral Dissertation Award, +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), -a 2021 Otto Hahn Medal -and the 2021 ETAPS Doctoral Dissertation Award. +an Otto Hahn Medal +and the ETAPS Doctoral Dissertation Award.

Download and references