From 9536235b85e75ce9bd9ab7f00732ab292b419039 Mon Sep 17 00:00:00 2001 From: Ralf Jung Date: Tue, 11 Jul 2017 13:36:01 -0700 Subject: [PATCH] https for plv.mpi-sws.org --- personal/_posts/2015-10-12-formalizing-rust.md | 4 ++-- personal/_posts/2017-07-08-rustbelt.md | 2 +- research/index.html | 4 ++-- research/publications.html | 4 ++-- 4 files changed, 7 insertions(+), 7 deletions(-) diff --git a/personal/_posts/2015-10-12-formalizing-rust.md b/personal/_posts/2015-10-12-formalizing-rust.md index 548fbd9..ad28165 100644 --- a/personal/_posts/2015-10-12-formalizing-rust.md +++ b/personal/_posts/2015-10-12-formalizing-rust.md @@ -15,7 +15,7 @@ It's going to be fun! Honestly, that's enough of a reason for me. 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. @@ -76,7 +76,7 @@ For example, to check that a function is semantically well-typed, you check what 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 diff --git a/personal/_posts/2017-07-08-rustbelt.md b/personal/_posts/2017-07-08-rustbelt.md index a37df23..9563866 100644 --- a/personal/_posts/2017-07-08-rustbelt.md +++ b/personal/_posts/2017-07-08-rustbelt.md @@ -25,7 +25,7 @@ used throughout the Rust ecosystem. -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` (inspired by [Abomonation](http://www.frankmcsherry.org/serialization/2015/05/04/unsafe-at-any-speed.html)). diff --git a/research/index.html b/research/index.html index 3b04268..825ee99 100644 --- a/research/index.html +++ b/research/index.html @@ -4,12 +4,12 @@ title: Ralf Jung
-

I am a PhD student at Max Planck Institute for Software Systems (MPI-SWS) and Saarland University under the supervision of Derek Dreyer, head of the Foundations of Programming group.

+

I am a PhD student at Max Planck Institute for Software Systems (MPI-SWS) and Saarland University under the supervision of Derek Dreyer, head of the Foundations of Programming group.

Previously, I did my Bachelor's thesis in computer science at the Compiler Design chair of the university (also see below).

I am currently working on giving a formal model to Rust's type system. -This work is part of the RustBelt project.
+This work is part of the RustBelt project.
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.
For some more information, check out my research blog.

diff --git a/research/publications.html b/research/publications.html index 7a21039..a12d648 100644 --- a/research/publications.html +++ b/research/publications.html @@ -39,7 +39,7 @@ slug: Publications Higher-Order Ghost State
Ralf Jung, Robbert Krebbers, Lars Birkedal, Derek Dreyer
In ICFP 2016: 21st ACM SIGPLAN International Conference on Functional Programming
- [paper] [project website (incl. appendix and Coq formalization)] [talk (YouTube)] [talk (slides)] + [paper] [project website (incl. appendix and Coq formalization)] [talk (YouTube)] [talk (slides)]

2015

@@ -55,7 +55,7 @@ slug: Publications Iris: Monoids and Invariants as an Orthogonal Basis for Concurrent Reasoning
Ralf Jung, David Swasey, Filip Sieczkowski, Kasper Svendsen, Aaron Turon, Lars Birkedal, Derek Dreyer
In POPL 2015: 42nd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages
- [paper] [project website (incl. appendix and Coq formalization)] [talk (slides)] + [paper] [project website (incl. appendix and Coq formalization)] [talk (slides)]

2013

-- 2.30.2