add some of my talks

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

diff --git a/personal/_posts/2017-07-08-rustbelt.md b/personal/_posts/2017-07-08-rustbelt.md
index 3342260ff5bfe7bad9eefd37fa0e7585cdf77206..2df2349e2c6aea3a70a891a059333d0cdbff4adb 100644 (file)
--- a/personal/_posts/2017-07-08-rustbelt.md
+++ b/personal/_posts/2017-07-08-rustbelt.md
@@ -25,11 +25,11 @@ used throughout the Rust ecosystem.
 
 <!-- MORE -->
 
 
 <!-- MORE -->
 

-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 %}).
+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]({% 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)).

-Our model of Rust is somewhat simplified (e.g., we don't support unwinding after panics); still, we were actually able to [find a real bug]({{ site.baseurl }}{% post_url 2017-06-09-mutexguard-sync %}).
+Our model of Rust is somewhat simplified (e.g., we don't support unwinding after panics); still, we were actually able to [find a real bug]({% post_url 2017-06-09-mutexguard-sync %}).

 For all the details, have a [look at the paper](https://www.mpi-sws.org/~dreyer/papers/rustbelt/paper.pdf).
 If that's not enough details for your taste, you can also check out [all our formal proofs](https://gitlab.mpi-sws.org/FP/LambdaRust-coq/).
 
 For all the details, have a [look at the paper](https://www.mpi-sws.org/~dreyer/papers/rustbelt/paper.pdf).
 If that's not enough details for your taste, you can also check out [all our formal proofs](https://gitlab.mpi-sws.org/FP/LambdaRust-coq/).
 


@@ -38,4 +38,6 @@ All these results were only possible because of my great collaborators, [Jacques
 I also benefited a lot from countless discussions with the Rust community at large, and with Aaron and Niko in particular.
 You guys rock!
 
 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:** 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**