From 2551c00778651228c1fd33f82fbefb1b5c249271 Mon Sep 17 00:00:00 2001
From: jihgfee <jihgfee@gmail.com>
Date: Tue, 27 Oct 2020 14:46:48 +0100
Subject: [PATCH] Addressed binder rules in README

---
 papers/LMCS.md | 16 ++++++++++++++++
 1 file changed, 16 insertions(+)

diff --git a/papers/LMCS.md b/papers/LMCS.md
index 9a28b20..3772e9b 100644
--- a/papers/LMCS.md
+++ b/papers/LMCS.md
@@ -16,3 +16,19 @@ Subprotocols
 Mechanisation
   - Program: [theories/examples/basics.v](../theories/examples/basics.v)
   - Subprotocol: [theories/examples/list_rev.v](../theories/examples/list_rev.v)
+
+## Differences between the formalization and the paper
+
+There are a number of small differences between the paper presentation
+of Actris 2.0 and the formalization in Coq, beyond those already covered
+in [papers/POPL20.md](POPL20.md), that are briefly discussed here.
+
+**Subprotocol rules with binders**
+
+The paper presents a set of rules for the subprotocol relation with binders,
+namely `⊑-send-mono'`, `⊑-recv-mono'`, and `⊑-swap'`. These are not available
+in the mechanisation, for technical reasons related to the encoding of binders.
+However, the rules are admissible from the primitive rules, as explained in the
+paper. The consequence of this is observed in the proof of the Löb recursion
+example, which differs from the proof presented in the paper, as it uses the
+rules with binders.
-- 
GitLab