From 698be0b84dea12a5fbc32798ad404b5b1092a2cd Mon Sep 17 00:00:00 2001
From: jihgfee <jihgfee@gmail.com>
Date: Sun, 10 May 2020 13:04:27 +0200
Subject: [PATCH] Added difference of ground type encoding

---
 papers/CONCUR20.md | 6 ++++++
 1 file changed, 6 insertions(+)

diff --git a/papers/CONCUR20.md b/papers/CONCUR20.md
index ae23ea2..79da91c 100644
--- a/papers/CONCUR20.md
+++ b/papers/CONCUR20.md
@@ -1,3 +1,9 @@
+## Differences
+
+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.
+
 ## Examples
 
 The parallel receive example in Section 4 can be found in
-- 
GitLab