add my PhD thesis

diff --git a/research/_config.yml b/research/_config.yml
index 67fc2a89bde2036f6cc6003884c4d8f9f639e0ce..4c1f1f93290ba95ad351966e37abf4929b71a64f 100644 (file)
--- a/research/_config.yml
+++ b/research/_config.yml
@@ -11,7 +11,7 @@ defaults:
 
 # Build settings
 markdown: kramdown
-exclude: ['*.sh', 'thesis.html']
+exclude: ['*.sh']
 
 # Custom settings
 mpi_sws_imprint: True

diff --git a/research/phd/thesis-print.pdf b/research/phd/thesis-print.pdf
new file mode 100644 (file)
index 0000000..7024a5e
Binary files /dev/null and b/research/phd/thesis-print.pdf differ

diff --git a/research/phd/thesis-screen.pdf b/research/phd/thesis-screen.pdf
new file mode 100644 (file)
index 0000000..d573631
Binary files /dev/null and b/research/phd/thesis-screen.pdf differ

diff --git a/research/thesis.html b/research/thesis.html
index 2510b236fee5de8852aa0ae21c46dfc775fd7b59..29ca0758696f137be11e718df782ab599f96f634 100644 (file)
--- a/research/thesis.html
+++ b/research/thesis.html
@@ -3,4 +3,17 @@ title: Understanding and Evolving the Rust Programming Language
 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</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>
+</p>