From: Ralf Jung
Date: Wed, 15 May 2019 19:05:05 +0000 (+0200)
Subject: typos
X-Git-Url: https://git.ralfj.de/web.git/commitdiff_plain/bf8063fb1a6c78e1bd8e808b5422e198b3949b62
typos
---
diff --git a/ralf/_posts/2019-05-15-typeclasses-exponential-blowup.md b/ralf/_posts/2019-05-15-typeclasses-exponential-blowup.md
index e59917b..2eda613 100644
--- a/ralf/_posts/2019-05-15-typeclasses-exponential-blowup.md
+++ b/ralf/_posts/2019-05-15-typeclasses-exponential-blowup.md
@@ -4,10 +4,10 @@ categories: research coq
forum: https://coq.discourse.group/t/blog-post-exponential-blowup-when-using-unbundled-typeclasses-to-model-algebraic-hierarchies/289
---
-When formalizing a proof in an interactive theorem prover like [Coq](https://coq.inria.fr/), one reoccuring issue is the handling of algebraic hierarchies.
+When formalizing a proof in an interactive theorem prover like [Coq](https://coq.inria.fr/), one reoccurring issue is the handling of algebraic hierarchies.
Such hierarchies are everywhere: some operations are associative, while others commute; some types have an equivalence relation, while others also have a (pre-)order or maybe even a well-ordering; and so on.
So the question arises: What is the best way to actually encode these hierarchies in Coq?
-Coq offers two mechanism that are suited to solve this task: typeclasses and canonical structures.
+Coq offers two mechanisms 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](http://www.eelis.net/research/math-classes/mscs.pdf).
However as we 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.