More differences

papers/CONCUR20.md

@@ -4,6 +4,11 @@ The semantic encoding of ground types use existential quantification in the
 mechanisation (e.g. `λ w. ∃ (x:Z), w = int`, while the paper uses set
 inclusion (e.g. `λ w. w ∈ Z`). The definitions are effectively identical.
 
+Polymorphism in the paper is done over the type kinds (e.g. `∀ (X :k).A`),
+where the mechanisation uses concrete types that are parametric on a kind
+(e.g. `∀ (X : lty k Σ).A`). This is just syntactic sugar to be less explicit
+in the paper.
+
 ## Examples
 
 The parallel receive example in Section 4 can be found in