X-Git-Url: https://git.ralfj.de/web.git/blobdiff_plain/5f79366c662bdd8c66d8ad1e207eba7dfca81d37..8a80fe7f85fc6ee9c6f4d4e85516b544998de57b:/personal/_drafts/typeclasses-exponential-blowup.md

diff --git a/personal/_drafts/typeclasses-exponential-blowup.md b/personal/_drafts/typeclasses-exponential-blowup.md
index ec6e6dd..bfff0ae 100644
--- a/personal/_drafts/typeclasses-exponential-blowup.md
+++ b/personal/_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).
-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.