Covered examples of LMCS submission in README and recovered POPL.md

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).

papers/LMCS.md

+## 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)

papers/POPL20.md

+
+## 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.