even more https

diff --git a/ralf/_drafts/typeclasses-exponential-blowup.md b/ralf/_drafts/typeclasses-exponential-blowup.md
index ec6e6dd2b725e4661bf566825fe32d3384e33359..bfff0aefe2c7c926a9880848405947e48b7a9d25 100644 (file)
--- a/ralf/_drafts/typeclasses-exponential-blowup.md
+++ b/ralf/_drafts/typeclasses-exponential-blowup.md
@@ -9,5 +9,5 @@ So the question arises:  What is the best way to actually encode these hierarchi
 Coq offers two mechanism that are suited to solve this task: typeclasses and canonical structures.
 Both can be instrumented in different ways to obtain a (more or less) convenient-to-use algebraic hierarchy.
 A common approach using typeclasses is the ["unbundled" approach by Bas Spitters and Eelis van der Weegen](https://arxiv.org/abs/1102.1323).
 Coq offers two mechanism that are suited to solve this task: typeclasses and canonical structures.
 Both can be instrumented in different ways to obtain a (more or less) convenient-to-use algebraic hierarchy.
 A common approach using typeclasses is the ["unbundled" approach by Bas Spitters and Eelis van der Weegen](https://arxiv.org/abs/1102.1323).

-However, as [has been observed before](https://pastel.archives-ouvertes.fr/pastel-00649586), and as learned the hard way in the Coq formalization of the [original Iris paper](http://iris-project.org/pdfs/2015-popl-iris1-final.pdf), this approach quickly leads to terms that seem to be exponential in size.
+However, as [has been observed before](https://pastel.archives-ouvertes.fr/pastel-00649586), and as learned the hard way in the Coq formalization of the [original Iris paper](https://iris-project.org/pdfs/2015-popl-iris1-final.pdf), this approach quickly leads to terms that seem to be exponential in size.

 
 

diff --git a/ralf/_posts/2015-10-12-formalizing-rust.md b/ralf/_posts/2015-10-12-formalizing-rust.md
index ad281658d932b5d6cd166c4d3adbc7fe755a6e36..43a1a710099c870734febcaa33256a3016aec64f 100644 (file)
--- a/ralf/_posts/2015-10-12-formalizing-rust.md
+++ b/ralf/_posts/2015-10-12-formalizing-rust.md
@@ -6,7 +6,7 @@ reddit: /rust/comments/3ofkz6/formalizing_rust/
 
 My current research project -- and the main topic of my PhD thesis -- is about developing a *semantic model* of the [Rust programming language](https://www.rust-lang.org/) and, most importantly, its type system.
 Rust is an attempt of Mozilla to find a sweet spot in the design space of programming languages: A language that provides low-level resource management (making it a systems language), is convenient for programmers and guards against memory errors and thread unsafety.
 
 My current research project -- and the main topic of my PhD thesis -- is about developing a *semantic model* of the [Rust programming language](https://www.rust-lang.org/) and, most importantly, its type system.
 Rust is an attempt of Mozilla to find a sweet spot in the design space of programming languages: A language that provides low-level resource management (making it a systems language), is convenient for programmers and guards against memory errors and thread unsafety.

-Other have [said](https://www.youtube.com/watch?v=O5vzLKg7y-k) and [written](http://www.oreilly.com/programming/free/files/why-rust.pdf) a lot on why we need such a language, so I won't lose any more words on this.
+Other have [said](https://www.youtube.com/watch?v=O5vzLKg7y-k) and [written](https://www.oreilly.com/programming/free/files/why-rust.pdf) a lot on why we need such a language, so I won't lose any more words on this.

 Let me just use this opportunity for a shameless plug: If you are curious and want to learn Rust, check out [Rust-101](https://www.ralfj.de/projects/rust-101/main.html), a hands-on Rust tutorial I wrote.
 I am going to assume some basic familiarity with Rust in the following.
 
 Let me just use this opportunity for a shameless plug: If you are curious and want to learn Rust, check out [Rust-101](https://www.ralfj.de/projects/rust-101/main.html), a hands-on Rust tutorial I wrote.
 I am going to assume some basic familiarity with Rust in the following.
 

diff --git a/ralf/_posts/2017-12-15-people-of-pl-interview.md b/ralf/_posts/2017-12-15-people-of-pl-interview.md
index 8722b4bbc36d648c6a9c76390a3090d8f999ccd5..27e40f49686ffaba0f887466da6c40967cb37204 100644 (file)
--- a/ralf/_posts/2017-12-15-people-of-pl-interview.md
+++ b/ralf/_posts/2017-12-15-people-of-pl-interview.md
@@ -14,7 +14,7 @@ Thanks a lot to Jean Yang, the Publicity Chair for POPL 2018, for making this a
 (Though, as you can see, I had to send them a picture, which was certainly the least pleasant part of this. ;)
 
 PS: It seems I have consistent bad luck with my POPL talk slots, because my talk
 (Though, as you can see, I had to send them a picture, which was certainly the least pleasant part of this. ;)
 
 PS: It seems I have consistent bad luck with my POPL talk slots, because my talk

-is [again](http://popl.mpi-sws.org/2015/program.html) in the very last session
+is [again](https://popl.mpi-sws.org/2015/program.html) in the very last session

 of the conference.  This time, in fact, it's the
 [very last talk](https://popl18.sigplan.org/program/program-POPL-2018?date=Fri%2012%20Jan%202018)
 of the main track.  Maybe some people read this interview and consider staying
 of the conference.  This time, in fact, it's the
 [very last talk](https://popl18.sigplan.org/program/program-POPL-2018?date=Fri%2012%20Jan%202018)
 of the main track.  Maybe some people read this interview and consider staying

diff --git a/ralf/_posts/2018-07-13-arc-synchronization.md b/ralf/_posts/2018-07-13-arc-synchronization.md
index e2a30c60d2566453aa7157e40fdfe6cabbdb203a..8363ac259678522afb60016012c4fa5e0af99114 100644 (file)
--- a/ralf/_posts/2018-07-13-arc-synchronization.md
+++ b/ralf/_posts/2018-07-13-arc-synchronization.md
@@ -8,7 +8,7 @@ While I was busy doing Rust-unrelated research, [RustBelt](https://plv.mpi-sws.o
 
 Notice that I am just the messenger here, the bug was actually found by [Hai](https://people.mpi-sws.org/~haidang/) and [Jacques-Henri](https://jhjourdan.mketjh.fr/).
 Still, I'd like to use this opportunity to talk a bit about weak memory, synchronization and data races.
 
 Notice that I am just the messenger here, the bug was actually found by [Hai](https://people.mpi-sws.org/~haidang/) and [Jacques-Henri](https://jhjourdan.mketjh.fr/).
 Still, I'd like to use this opportunity to talk a bit about weak memory, synchronization and data races.

-This is just a primer, there are tons of resources on the web that go into more detail (for example [here](http://preshing.com/20120913/acquire-and-release-semantics/)).
+This is just a primer, there are tons of resources on the web that go into more detail (for example [here](https://preshing.com/20120913/acquire-and-release-semantics/)).

 
 <!-- MORE -->
 
 
 <!-- MORE -->