From a34d13a6c7be5f9f2f9a88aeba6318ad02263ab1 Mon Sep 17 00:00:00 2001
From: Jonas <jihgfee@gmail.com>
Date: Thu, 21 Nov 2019 19:30:45 -0500
Subject: [PATCH] Added description of subtyping discrepancy in the README

---
 README.md | 11 +++++++++++
 1 file changed, 11 insertions(+)

diff --git a/README.md b/README.md
index cda5866..0c56c73 100644
--- a/README.md
+++ b/README.md
@@ -154,3 +154,14 @@ of Actris and the formalization in Coq, that are briefly discussed here.
   1. the `â–¶` in the CPS encoding of protocols,
   2. the higher-order ghost state used for ownership of protocols, and
   3. the opening of the protocol invariant.
+
+- **Subtyping relation in c↣ prot**
+
+  The mechanisation has introduced the notion of subtyping, which allows one to
+  strengten/weaken the predicates of sends/receives respectively. In particular
+  this means that the endpoint ownership has been extended with `iProto_le p p'`,
+  where `p'` is the original protocol used in the ghost state, and `p` is the
+  protocol denoted by the ownership `c↣ prot`. The effect of this is that the
+  user can update his own view of the protocol, as long as it is consistent
+  with the original protocol in the invariant. As such the fundamental aspect of
+  the ownership still align with that of the paper.
\ No newline at end of file
-- 
GitLab