provenance-matters: explain what went wrong

[web.git] / research / thesis.html

diff --git a/research/thesis.html b/research/thesis.html
index 2510b236fee5de8852aa0ae21c46dfc775fd7b59..1ad155d991fe0386ed1688c1ab2037a3eac2fc98 100644 (file)
--- a/research/thesis.html
+++ b/research/thesis.html
@@ -3,4 +3,18 @@ title: Understanding and Evolving the Rust Programming Language
 slug: Thesis
 ---
 
 slug: Thesis
 ---
 

-This is where my PhD thesis will be made available.
+<p><em>Rust</em> is a young systems programming language that aims to fill the gap between <em>high-level languages</em>—which provide strong static guarantees like memory and thread safety—and <em>low-level languages</em>—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 <em>understand</em> and <em>evolve</em> this important language: <em>RustBelt</em> and <em>Stacked Borrows</em>.</p>
+
+<p><em>RustBelt</em> 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 <em>unsafe</em> language features.</p>
+
+<p><em>Stacked Borrows</em> is a proposed extension of the Rust specification, which enables the compiler to use the strong aliasing information in Rust’s types to better analyze and optimize the code it is compiling. The adequacy of this specification is evaluated not only formally, but also by running real Rust code in an instrumented version of Rust’s <em>Miri</em> interpreter that implements the Stacked Borrows semantics.</p>
+
+<p>RustBelt is built on top of <em>Iris</em>, 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 <em>lifetime logic</em>, which provides a novel separation-logic account of <em>borrowing</em>, a key distinguishing feature of the Rust type system.</p>
+
+<h3>Download and references</h3>
+
+<ul>
+<li><a href="phd/thesis-screen.pdf">Screen-optimized version (PDF)</a></li>
+<li><a href="phd/thesis-print.pdf">Print-optimized version (PDF)</a></li>
+<li>DOI: <a href="http://dx.doi.org/10.22028/D291-31946">10.22028/D291-31946</a></li>
+</ul>