But there are other reasons: It shouldn't be a surprise that [bugs](https://github.com/rust-lang/rust/issues/24292) have [been](https://github.com/rust-lang/rust/issues/25860) [found](https://github.com/rust-lang/rust/issues/24880) in Rust.
There are lots of things that can be done about such bugs -- my take on this is that we should try to *prove*, in a mathematical rigorous way, that no such bugs exist in Rust.
This goes hand-in-hand with other approaches like testing, fuzzing and [static analysis](https://homes.cs.washington.edu/~emina/pubs/crust.ase15.pdf).
-However, we (at my [research group](http://plv.mpi-sws.org/)) are into formalizing things, so that's what we are going to do as part of the [RustBelt](http://plv.mpi-sws.org/rustbelt/) research project.
+However, we (at my [research group](https://plv.mpi-sws.org/)) are into formalizing things, so that's what we are going to do as part of the [RustBelt](https://plv.mpi-sws.org/rustbelt/) research project.
**Update:** Added link to RustBelt website.
It doesn't matter *how* the function performs these operations.
This is in contrast to the *syntactic* notion of well-typedness of a function, which involves looking at the *code* of the function and checking it against a bunch of rules.
Only recently, research has been able to scale up such semantic methods to languages that combine state (i.e., mutable variables, a heap) with higher-order functions -- languages like Rust, where I can take a closure (a `Fn{,Mut,Once}`) and store it in memory, for later use.
-Lucky enough, my advisor [Derek Dreyer](http://www.mpi-sws.org/~dreyer/) is one of the world experts in this field, which permits me to intensively study Rust (which I would have done anyways) and call it research!
+Lucky enough, my advisor [Derek Dreyer](https://www.mpi-sws.org/~dreyer/) is one of the world experts in this field, which permits me to intensively study Rust (which I would have done anyways) and call it research!
## What We Are Doing
<!-- 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)).
<div style="float:right; margin-left:0.8em; margin-bottom: 0.3em"><img src="me.jpg"></div>
-<p>I am a PhD student at <a href="http://www.mpi-sws.org/" target="_blank">Max Planck Institute for Software Systems (MPI-SWS)</a> and <a href="http://www.uni-saarland.de/" target="_blank">Saarland University</a> under the supervision of <a href="http://www.mpi-sws.org/~dreyer/" target="_blank">Derek Dreyer</a>, head of the <a href="http://plv.mpi-sws.org/" target="_blank">Foundations of Programming group</a>.</p>
+<p>I am a PhD student at <a href="http://www.mpi-sws.org/" target="_blank">Max Planck Institute for Software Systems (MPI-SWS)</a> and <a href="http://www.uni-saarland.de/" target="_blank">Saarland University</a> under the supervision of <a href="http://www.mpi-sws.org/~dreyer/" target="_blank">Derek Dreyer</a>, head of the <a href="https://plv.mpi-sws.org/" target="_blank">Foundations of Programming group</a>.</p>
<p>Previously, I did my Bachelor's thesis in computer science at the <a href="http://www.cdl.uni-saarland.de/index.php">Compiler Design chair</a> of the university (also see below).</p>
<p>I am currently working on giving a formal model to <a href="https://www.rust-lang.org/">Rust's</a> type system.
-This work is part of the <a href="http://plv.mpi-sws.org/rustbelt/">RustBelt</a> project. <br/>
+This work is part of the <a href="https://plv.mpi-sws.org/rustbelt/">RustBelt</a> project. <br/>
The Rust work builds on my previous work on a logic to support modular reasoning about higher-order concurrent imperative programs. The focus there was on providing simple building blocks that are powerful enough to recover more sophisticated reasoning techniques that were often axiomatized in previous logics. <br/>
For some more information, check out my <a href="https://www.ralfj.de/blog/categories/research.html">research blog</a>.</p>
<b>Higher-Order Ghost State</b><br/>
Ralf Jung, Robbert Krebbers, Lars Birkedal, Derek Dreyer<br>
In <a href="http://conf.researchr.org/home/icfp-2016">ICFP 2016</a>: 21st ACM SIGPLAN International Conference on Functional Programming<br>
- [<a href="http://iris-project.org/pdfs/2016-icfp-iris2-final.pdf">paper</a>] [<a href="http://
plv.mpi-sws.org/iris/">project website</a> (incl. appendix and Coq formalization)] [<a href="https://www.youtube.com/watch?v=vUxWU-qvGX0" target="_blank">talk (YouTube)</a>] [<a href="iris/talk-icfp2016.pdf">talk (slides)</a>]
+ [<a href="http://iris-project.org/pdfs/2016-icfp-iris2-final.pdf">paper</a>] [<a href="http://
iris-project.org">project website</a> (incl. appendix and Coq formalization)] [<a href="https://www.youtube.com/watch?v=vUxWU-qvGX0" target="_blank">talk (YouTube)</a>] [<a href="iris/talk-icfp2016.pdf">talk (slides)</a>]
</li></ul>
<h3>2015</h3>
<b>Iris: Monoids and Invariants as an Orthogonal Basis for Concurrent Reasoning</b><br/>
Ralf Jung, David Swasey, Filip Sieczkowski, Kasper Svendsen, Aaron Turon, Lars Birkedal, Derek Dreyer<br>
In <a href="http://popl.mpi-sws.org/2015/">POPL 2015</a>: 42nd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages<br>
- [<a href="http://iris-project.org/pdfs/2015-popl-iris1-final.pdf">paper</a>] [<a href="http://
plv.mpi-sws.org/iris/">project website</a> (incl. appendix and Coq formalization)] [<a href="iris/talk-popl2015.pdf">talk (slides)</a>]
+ [<a href="http://iris-project.org/pdfs/2015-popl-iris1-final.pdf">paper</a>] [<a href="http://
iris-project.org">project website</a> (incl. appendix and Coq formalization)] [<a href="iris/talk-popl2015.pdf">talk (slides)</a>]
</li></ul>
<h3>2013</h3>
projects / web.git / commitdiff