add reddit link master
authorRalf Jung <post@ralfj.de>
Tue, 19 Nov 2019 19:18:05 +0000 (20:18 +0100)
committerRalf Jung <post@ralfj.de>
Tue, 19 Nov 2019 19:18:05 +0000 (20:18 +0100)
ralf/_posts/2019-10-20-type-soundness.md [new file with mode: 0644]
ralf/_posts/2019-11-18-stacked-borrows-paper.md [new file with mode: 0644]
research/publications.html

diff --git a/ralf/_posts/2019-10-20-type-soundness.md b/ralf/_posts/2019-10-20-type-soundness.md
new file mode 100644 (file)
index 0000000..a8b9dbb
--- /dev/null
@@ -0,0 +1,14 @@
+---
+title: 'What Type Soundness Theorem Do You Really Want to Prove?'
+categories: rust research
+---
+
+My advisor Derek and some of my coauthors Amin, Robbert and Lars just put out a blog post on the [SIGPLAN blog](https://blog.sigplan.org/) on the idea of "semantic typing".
+This is the methodology behind [RustBelt](https://plv.mpi-sws.org/rustbelt/popl18/), so the post is a great starting point for understanding the context of that paper and the key bits of prior research that it rests on.
+In fact they used Rust as their main example language for that post, and I helped them out a bit with some of the technical details there so they kindly added me to the author list.
+
+The approach they describe is much more widely applicable than Rust though; it provides a whole new perspective on type systems that I think deserves way more attention than it gets.
+If you are interested in formal methods for type systems and in particular for Rust, you should check it out!
+It's a great read:
+
+> ["What Type Soundness Theorem Do You Really Want to Prove?" on *PL Perspectives*](https://blog.sigplan.org/2019/10/17/what-type-soundness-theorem-do-you-really-want-to-prove/)
diff --git a/ralf/_posts/2019-11-18-stacked-borrows-paper.md b/ralf/_posts/2019-11-18-stacked-borrows-paper.md
new file mode 100644 (file)
index 0000000..49d7dc7
--- /dev/null
@@ -0,0 +1,24 @@
+---
+title: "Stacked Borrows: An Aliasing Model for Rust (the paper)"
+categories: research rust
+reddit: /rust/comments/dy8avz/stacked_borrows_an_aliasing_model_for_rust_the/
+---
+
+I have [blogged]({% post_url 2019-05-21-stacked-borrows-2.1 %}) a [few]({% post_url 2019-04-30-stacked-borrows-2 %}) times before about [Stacked Borrows](https://github.com/rust-lang/unsafe-code-guidelines/blob/master/wip/stacked-borrows.md), my proposed aliasing model for Rust.
+But I am a researcher, and what researchers (are expected to) do is write papers---so that's what we did for Stacked Borrows as well.
+After a lot of work, I can now finally present to you our paper [Stacked Borrows: An Aliasing Model for Rust](https://plv.mpi-sws.org/rustbelt/stacked-borrows/) (thanks to open access, the paper is available under the CC-BY 4.0 license).
+
+<!-- MORE -->
+
+If you have already read my blog posts, the paper does not say much you have not seen already.
+However, the paper is the most coherent and most complete introduction to Stacked Borrows so far.
+So if you were always confused by some aspect of Stacked Borrows, or if you have not read the previous blog posts, the paper is a great way to learn about Stacked Borrows.
+
+If there is nothing new, you may wonder what took us so long, then, and why we needed 4 people for that?
+The answer is that my coauthor Hai, with some help from Jeehoon and me, took on the Herculean task of [formalizing Stacked Borrows in Coq](https://gitlab.mpi-sws.org/FP/stacked-borrows) and then formally verifying that some key optimizations are actually sound under that model.
+Those proofs turned out to be more complex to carry out than we expected, but now I am sure that what I claimed about Stacked Borrows in previous posts is actually correct.
+(In fact we were not able to complete the proof in time for the conference submission deadline, but lucky enough the reviewers were convinced enough by the informal description and the evaluation with Miri that they still accepted the paper.)
+
+Let me also use this opportunity to thank Mozilla and the Rust community for their help with this project.
+This work would not have been possible without Mozilla hiring me for two internships, without all the great feedback that you all gave me in response to my blog posts, and without all the support that I got in implementing Stacked Borrows, testing the standard library and a growing number of external crates in Miri, and fixing Stacked Borrows errors as they came up.
+Thank you all so much for working with me on this, this has been (and will hopefully continue to be) great fun. :-)
index e2b610f..135f77d 100644 (file)
@@ -5,6 +5,22 @@ slug: Publications
 
 <!-- <h3>Under Submission</h3> -->
 
+<h3>2020</h3>
+
+<ul><li>
+  <b>The Future is Ours: Prophecy Variables in Separation Logic</b><br/>
+  Ralf Jung, Rodolphe Lepigre, Gaurav Parthasarathy, Marianna Rapoport, Amin Timany, Derek Dreyer, Bart Jacobs<br>
+  In <a href="https://popl20.sigplan.org/">POPL 2020</a><br>
+  [<a href="https://plv.mpi-sws.org/prophecies/paper.pdf">paper</a>] [<a href="https://plv.mpi-sws.org/prophecies/">paper website</a>  (incl. appendix and Coq formalization)]
+</li></ul>
+
+<ul><li>
+  <b>Stacked Borrows: An Aliasing Model for Rust</b><br/>
+  Ralf Jung, Hoang-Hai Dang, Jeehoon Kang, Derek Dreyer<br>
+  In <a href="https://popl20.sigplan.org/">POPL 2020</a><br>
+  [<a href="https://plv.mpi-sws.org/rustbelt/stacked-borrows/paper.pdf">paper</a>] [<a href="https://plv.mpi-sws.org/rustbelt/stacked-borrows/">paper website</a>  (incl. appendix and Coq formalization)]
+</li></ul>
+
 <h3>2018</h3>
 
 <ul><li>