diff --git a/README.md b/README.md
index 72903ee7fd593d2a1fdc91a5de40a003efe74c5d..caee319daeae54954aa159e1f2ecb0a20d99aac9 100644
--- a/README.md
+++ b/README.md
@@ -57,6 +57,8 @@ Dependent Separation Protocols:
 | Append | `prot_1 · prot_2`             | `prot_1 <++> prot_2`                  |
 | Dual   | An overlined protocol         | No notation                           |
 
+This notation is additionally used for the LMCS submission.
+
 Semantic Session Types:
 
 |          | CPP21 submission              | Coq mechanization                     |
@@ -175,4 +177,6 @@ the values of the list made explicit.
 ## Paper-specific remarks
 
 For remarks about the CPP21 submission, see
+[papers/POPL20.md](papers/POPL20.md).
 [papers/CPP21.md](papers/CPP21.md).
+[papers/LMCS.md](papers/LMCS.md).
diff --git a/papers/LMCS.md b/papers/LMCS.md
new file mode 100644
index 0000000000000000000000000000000000000000..9a28b202695df7744a03e5a3b78b5c4da600839a
--- /dev/null
+++ b/papers/LMCS.md
@@ -0,0 +1,18 @@
+## Examples
+
+The examples of the original POPL20 paper are covered in
+[papers/POPL20.md](POPL20.md).
+
+The following list gives a mapping between the additional examples in the
+paper and their mechanization in Coq:
+
+Introduction
+  - Swapping program: [theories/examples/basics.v](../theories/examples/basics.v)
+Subprotocols
+  - Basics: [theories/examples/subprotocols.v](../theories/examples/subprotocols.v)
+  - Mapper: [theories/examples/swap_mapper.v](../theories/examples/swap_mapper.v)
+  - List reversal: [theories/examples/list_rev.v](../theories/examples/list_rev.v)
+  - Löb recursion: [theories/examples/subprotocols.v](../theories/examples/subprotocols.v)
+Mechanisation
+  - Program: [theories/examples/basics.v](../theories/examples/basics.v)
+  - Subprotocol: [theories/examples/list_rev.v](../theories/examples/list_rev.v)
diff --git a/papers/POPL20.md b/papers/POPL20.md
new file mode 100644
index 0000000000000000000000000000000000000000..8a2b7224a161fd74995a9dcaa16ebcdfb3434d7b
--- /dev/null
+++ b/papers/POPL20.md
@@ -0,0 +1,59 @@
+
+## Examples
+
+The examples can be found in the directory [theories/examples](../theories/examples).
+
+The following list gives a mapping between the examples in the paper and their
+mechanization in Coq:
+
+Introduction: [theories/examples/basics.v](../theories/examples/basics.v)
+Tour of Actris
+  - Basics: [theories/examples/sort.v](../theories/examples/sort.v)
+  - Higher-Order Functions: [theories/examples/sort.v](../theories/examples/sort.v)
+  - Branching: [theories/examples/sort_br_del.v](../theories/examples/sort_br_del.v)
+  - Recursion: [theories/examples/sort_br_del.v](../theories/examples/sort_br_del.v)
+  - Delegation: [theories/examples/sort_br_del.v](../theories/examples/sort_br_del.v)
+  - Dependent: [theories/examples/sort_fg.v](../theories/examples/sort_fg.v)
+Manifest sharing via locks
+  - Sample program: [theories/examples/basics.v](../theories/examples/basics.v)
+  - Distributed mapper: [theories/examples/map.v](../theories/examples/map.v)
+Case study: map reduce:
+  - Utilities for shuffling/grouping: [theories/utils/group.v](../theories/utils/group.v)
+  - Implementation and verification: [theories/examples/map_reduce.v](../theories/examples/map_reduce.v)
+
+## Differences between the formalization and the paper
+
+There are a number of small differences between the paper presentation
+of Actris and the formalization in Coq, that are briefly discussed here.
+
+**Weakest preconditions versus Hoare triples**
+
+The presentation of the Actris logic in the paper makes use of Hoare triples.
+In Coq, we make use of weakest preconditions because these are more convenient for
+interactive theorem proving using the the [proof mode tactics][ProofMode]. To
+state concise program specifications, we use the notion of *Texan Triples* from
+Iris, which provides a convenient "Hoare triple"-like syntax around weakest
+preconditions:
+
+```
+{{{ P }}} e {{{ x .. y, RET v; Q }}} :=
+  □ ∀ Φ, P -∗ ▷ (∀ x .. y, Q -∗ Φ v) -∗ WP e {{ Φ }}
+```
+
+**Connectives for physical ownership of channels**
+
+In the paper, physical ownership of a channel is formalized using a single
+connective `(c1,c2) ↣ (vs1,vs2)`. Since then we have made the Actris
+hoare triples the primitive specification for the channels, and instead
+defined channel ownership directly in terms of the buffer ownership
+`llist internal_eq l vs1` and `llist intenral_eq r vs2` for channels
+`(l,r,lk)` and `(r,l,lk)`.
+
+**Protocol subtyping**
+
+The mechanization has introduced the notion of "protocol subtyping", which
+allows one to strengthen/weaken the predicates of sends/receives, respectively.
+This is achieved using the relation `iProto_le p p'`, and the additional rule
+`c ↣ p -∗ iProto_le p p' -∗ c ↣ p'`. To support "protocol subtyping", the
+definition of `c ↣ p` in the model is changed to be closed under `iProto_le`.
+This idea is formally presented in the LMCS submission.