more https

diff --git a/ralf/projects/index.md b/ralf/projects/index.md
index 72fbb7cd97929096c382b20ed3f14c1b76e5e668..c5d3f4aa47753dbf3db6dfbe80087bec6e1b60f9 100644 (file)
--- a/ralf/projects/index.md
+++ b/ralf/projects/index.md
@@ -16,7 +16,7 @@ But maybe you are having just the same problem as I did, in which case I hope th
 * [schsh](schsh/): A collection of scripts and configuration files which can be used to grant
   someone secure (SSH-based) access to a machine, without giving them a shell or read access
   to the entire file system.
-* [Rust-101](rust-101/): A small tutorial for the [Rust language](http://www.rust-lang.org).
+* [Rust-101](rust-101/): A small tutorial for the [Rust language](https://www.rust-lang.org).
 * [git-mirror](git-mirror/): This can keep multiple git repositories of the same project in sync automatically.
 
 For some more of my projects, check out the [public git repositories](https://www.ralfj.de/git/)

diff --git a/research/index.html b/research/index.html
index 825ee99a254656de8ca8a6f4064695ffd12e1bf5..14eb3c24b684fb2d9029a48f1326b35770d782c2 100644 (file)
--- a/research/index.html
+++ b/research/index.html
@@ -4,7 +4,7 @@ title: Ralf Jung
 
 <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="https://plv.mpi-sws.org/" target="_blank">Foundations of Programming group</a>.</p>
+<p>I am a PhD student at <a href="https://www.mpi-sws.org/" target="_blank">Max Planck Institute for Software Systems (MPI-SWS)</a> and <a href="https://www.uni-saarland.de/" target="_blank">Saarland University</a> under the supervision of <a href="https://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>
 

diff --git a/research/publications.html b/research/publications.html
index 5b30140ea288917094269b959a961a3dd09d44d8..71d6be50ba486e0085178902937f6911ef2780ac 100644 (file)
--- a/research/publications.html
+++ b/research/publications.html
@@ -8,7 +8,7 @@ slug: Publications
 <ul><li>
   <b>Iris from the Ground Up: A Modular Foundation for Higher-Order Concurrent Separation Logic</b><br/>
   Ralf Jung, Robbert Krebbers, Jacques-Henri Jourdan, Aleš Bizjak, Lars Birkedal, Derek Dreyer<br>
-  [<a href="http://www.mpi-sws.org/~dreyer/papers/iris-ground-up/paper.pdf">preprint</a>] [<a href="http://iris-project.org">project website</a>  (incl. appendix and Coq formalization)]
+  [<a href="https://www.mpi-sws.org/~dreyer/papers/iris-ground-up/paper.pdf">preprint</a>] [<a href="https://iris-project.org">project website</a>  (incl. appendix and Coq formalization)]
 </li></ul>
 
 <h3>2018</h3>
@@ -17,7 +17,7 @@ slug: Publications
   <b>MoSeL: A General, Extensible Modal Framework for Interactive Proofs in Separation Logic</b><br/>
   Robbert Krebbers, Jacques-Henri Jourdan, Ralf Jung, Joseph Tassarotti, Jan-Oliver Kaiser, Amin Timany, Arthur Charguéraud, Derek Dreyer<br>
   In <a href="https://icfp18.sigplan.org/">ICFP 2018</a>: 23nd ACM SIGPLAN International Conference on Functional Programming<br>
-  [<a href="http://iris-project.org/pdfs/2018-icfp-mosel-final.pdf">paper</a>] [<a href="http://iris-project.org/mosel/">paper website</a>  (incl. appendix and Coq formalization)]
+  [<a href="https://iris-project.org/pdfs/2018-icfp-mosel-final.pdf">paper</a>] [<a href="https://iris-project.org/mosel/">paper website</a>  (incl. appendix and Coq formalization)]
 </li></ul>
 
 <ul><li>
@@ -32,15 +32,15 @@ slug: Publications
 <ul><li>
   <b>The Essence of Higher-Order Concurrent Separation Logic</b><br/>
   Robbert Krebbers, Ralf Jung, Aleš Bizjak, Jacques-Henri Jourdan, Derek Dreyer, Lars Birkedal<br>
-  In <a href="http://www.etaps.org/index.php/2017/esop">ESOP 2017</a>: 26th European Symposium on Programming<br>
-  [<a href="http://iris-project.org/pdfs/2017-esop-iris3-final.pdf">paper</a>] [<a href="http://iris-project.org">project website</a>  (incl. appendix and Coq formalization)]
+  In <a href="https://www.etaps.org/index.php/2017/esop">ESOP 2017</a>: 26th European Symposium on Programming<br>
+  [<a href="https://iris-project.org/pdfs/2017-esop-iris3-final.pdf">paper</a>] [<a href="https://iris-project.org">project website</a>  (incl. appendix and Coq formalization)]
 </li></ul>
 
 <ul><li>
   <b>A Higher-Order Logic for Concurrent Termination-Preserving Refinement</b><br/>
   Joseph Tassarotti, Ralf Jung, Robert Harper<br>
-  In <a href="http://www.etaps.org/index.php/2017/esop">ESOP 2017</a>: 26th European Symposium on Programming<br>
-  [<a href="http://iris-project.org/pdfs/2017-esop-refinement-final.pdf">paper</a>] [<a href="https://www.cs.cmu.edu/~jtassaro/papers/iris-refinement/index.html">paper website</a> (incl. Coq formalization)]
+  In <a href="https://www.etaps.org/index.php/2017/esop">ESOP 2017</a>: 26th European Symposium on Programming<br>
+  [<a href="https://iris-project.org/pdfs/2017-esop-refinement-final.pdf">paper</a>] [<a href="https://www.cs.cmu.edu/~jtassaro/papers/iris-refinement/index.html">paper website</a> (incl. Coq formalization)]
 </li></ul>
 
 <h3>2016</h3>
@@ -48,8 +48,8 @@ slug: Publications
 <ul><li>
   <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://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>]
+  In <a href="https://conf.researchr.org/home/icfp-2016">ICFP 2016</a>: 21st ACM SIGPLAN International Conference on Functional Programming<br>
+  [<a href="https://iris-project.org/pdfs/2016-icfp-iris2-final.pdf">paper</a>] [<a href="https://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>
@@ -57,15 +57,15 @@ slug: Publications
 <ul><li>
   <b>Unifying Worlds and Resources</b><br/>
   Ralf Jung, Derek Dreyer<br>
-  In <a href="http://users-cs.au.dk/birke/hope-2015/">HOPE 2015</a>: 4th ACM SIGPLAN Workshop on Higher-Order Programming with Effects<br>
+  In <a href="https://users-cs.au.dk/birke/hope-2015/">HOPE 2015</a>: 4th ACM SIGPLAN Workshop on Higher-Order Programming with Effects<br>
   [<a href="https://www.youtube.com/watch?v=9Dyna88piek&amp;list=PLnqUlCo055hX6SsmMr1AmW6quMjvdMPvK&amp;index=10" target="_blank">talk (YouTube)</a>] [<a href="iris/talk-hope2015.pdf">talk (slides)</a>]
 </li></ul>
 
 <ul><li>
   <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://iris-project.org">project website</a>  (incl. appendix and Coq formalization)] [<a href="iris/talk-popl2015.pdf">talk (slides)</a>]
+  In <a href="https://popl.mpi-sws.org/2015/">POPL 2015</a>: 42nd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages<br>
+  [<a href="https://iris-project.org/pdfs/2015-popl-iris1-final.pdf">paper</a>] [<a href="https://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>