https for plv.mpi-sws.org

diff --git a/personal/_posts/2015-10-12-formalizing-rust.md b/personal/_posts/2015-10-12-formalizing-rust.md
index 548fbd9297a6dc9b67814ad768c454d905a27166..ad281658d932b5d6cd166c4d3adbc7fe755a6e36 100644 (file)
--- 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).
 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.
 
 
 **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.
 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
 
 
 ## What We Are Doing
 

diff --git a/personal/_posts/2017-07-08-rustbelt.md b/personal/_posts/2017-07-08-rustbelt.md
index a37df23e86e84da08e85c8feb1fd960a16b6096a..95638667d461c7e82c4dd8e259eea0dbf190c72e 100644 (file)
--- 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.
 
 <!-- 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)).

diff --git a/research/index.html b/research/index.html
index 3b04268a4df7fe9bc2a30dcae33e33eea9e15197..825ee99a254656de8ca8a6f4064695ffd12e1bf5 100644 (file)
--- a/research/index.html
+++ b/research/index.html
@@ -4,12 +4,12 @@ title: Ralf Jung
 
 <div style="float:right; margin-left:0.8em; margin-bottom: 0.3em"><img src="me.jpg"></div>
 
 
 <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.
 
 <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>
 
 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>
 

diff --git a/research/publications.html b/research/publications.html
index 7a210391e098a8aa95325fa968a1db7b818831da..a12d648a3dfe1aa15644318b8fc0d71628031cea 100644 (file)
--- a/research/publications.html
+++ b/research/publications.html
@@ -39,7 +39,7 @@ slug: Publications
   <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>
   <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>
 </li></ul>
 
 <h3>2015</h3>


@@ -55,7 +55,7 @@ slug: Publications
   <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>
   <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>
 </li></ul>
 
 <h3>2013</h3>