link to compcert

[web.git] / ralf / _posts / 2017-07-08-rustbelt.md

diff --git a/ralf/_posts/2017-07-08-rustbelt.md b/ralf/_posts/2017-07-08-rustbelt.md
index a37df23e86e84da08e85c8feb1fd960a16b6096a..1dfee5b99eec2a9c4bc8e8ddde90ceeb3ff9013d 100644 (file)
--- a/ralf/_posts/2017-07-08-rustbelt.md
+++ b/ralf/_posts/2017-07-08-rustbelt.md
@@ -4,7 +4,7 @@ categories: research rust
 forum: https://internals.rust-lang.org/t/rustbelt-securing-the-foundations-of-the-rust-programming-language/5509
 ---
 
 forum: https://internals.rust-lang.org/t/rustbelt-securing-the-foundations-of-the-rust-programming-language/5509
 ---
 

-Just yesterday, we submitted our paper [RustBelt: Securing the Foundations of the Rust Programming Language](https://www.mpi-sws.org/~dreyer/papers/rustbelt/paper.pdf).
+Just yesterday, we submitted our paper [RustBelt: Securing the Foundations of the Rust Programming Language](https://plv.mpi-sws.org/rustbelt/popl18/).

 Quoting from the abstract:
 
 > Rust is a new systems programming language that promises to overcome
 Quoting from the abstract:
 
 > Rust is a new systems programming language that promises to overcome


@@ -25,7 +25,7 @@ used throughout the Rust ecosystem.
 
 <!-- MORE -->
 
 
 <!-- MORE -->
 

-This paper is the result of almost two years of work by the [RustBelt](http://plv.mpi-sws.org/rustbelt/) research project to [formalize Rust's type system]({{ site.baseurl }}{% post_url 2015-10-12-formalizing-rust %}).
+This paper is the result of almost two years of work by the [RustBelt](https://plv.mpi-sws.org/rustbelt/) research project to [formalize Rust's type system]({{ site.baseurl }}{% post_url 2015-10-12-formalizing-rust %}).

 The paper is now undergoing peer review; some time in fall we will be notified whether the paper got accepted or not.
 
 In case you wondered which "important libraries" we verified, the full list is `Rc`, `Arc`, `Cell` (including [`alias::one`](https://huonw.github.io/alias/alias/fn.one.html), which was recently [accepted into the standard library](https://github.com/rust-lang/rfcs/pull/1789)), `RefCell`, `Mutex`, `RwLock`, `thread::spawn`, `mem::swap`, [`take_mut::take`](https://docs.rs/take_mut/0.1.3/take_mut/fn.take.html) as well as converting `&&T` into `&Box<T>` (inspired by [Abomonation](http://www.frankmcsherry.org/serialization/2015/05/04/unsafe-at-any-speed.html)).
 The paper is now undergoing peer review; some time in fall we will be notified whether the paper got accepted or not.
 
 In case you wondered which "important libraries" we verified, the full list is `Rc`, `Arc`, `Cell` (including [`alias::one`](https://huonw.github.io/alias/alias/fn.one.html), which was recently [accepted into the standard library](https://github.com/rust-lang/rfcs/pull/1789)), `RefCell`, `Mutex`, `RwLock`, `thread::spawn`, `mem::swap`, [`take_mut::take`](https://docs.rs/take_mut/0.1.3/take_mut/fn.take.html) as well as converting `&&T` into `&Box<T>` (inspired by [Abomonation](http://www.frankmcsherry.org/serialization/2015/05/04/unsafe-at-any-speed.html)).


@@ -37,3 +37,7 @@ Of course, I am far from the only person who worked on this.
 All these results were only possible because of my great collaborators, [Jacques-Henri Jourdan](https://jhjourdan.mketjh.fr/) and [Robbert Krebbers](http://robbertkrebbers.nl/), as well as my PhD advisor, [Derek Dreyer](http://www.mpi-sws.org/~dreyer/).
 I also benefited a lot from countless discussions with the Rust community at large, and with Aaron and Niko in particular.
 You guys rock!
 All these results were only possible because of my great collaborators, [Jacques-Henri Jourdan](https://jhjourdan.mketjh.fr/) and [Robbert Krebbers](http://robbertkrebbers.nl/), as well as my PhD advisor, [Derek Dreyer](http://www.mpi-sws.org/~dreyer/).
 I also benefited a lot from countless discussions with the Rust community at large, and with Aaron and Niko in particular.
 You guys rock!

+
+**Update:** I have changed the link to point to the [final version of the paper](https://plv.mpi-sws.org/rustbelt/popl18/). **/Update**
+
+**Update:** The conference talk is now available [on YouTube](https://www.youtube.com/watch?v=Cy9NUVaiYUg). **/Update**