From: Ralf Jung Date: Fri, 7 Oct 2022 15:35:24 +0000 (+0200) Subject: syntax X-Git-Url: https://git.ralfj.de/web.git/commitdiff_plain/4d2435b3d268f5f592fd2cec16f35b6a13a5ef51?ds=sidebyside;hp=ff279676c168508b0d9eb7a0b31e9b7d93713863 syntax --- diff --git a/research/thesis.html b/research/thesis.html index 926141f..89f7328 100644 --- a/research/thesis.html +++ b/research/thesis.html @@ -16,7 +16,7 @@ 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,