Merge branch 'concur2020' into 'master'

Concur2020

See merge request iris/actris!20

README.md

 # ACTRIS COQ DEVELOPMENT
 
+For CONCUR 2020 specific remarks see [CONCUR2020.md](CONCUR2020.md).
+
 This directory contains the Coq mechanisation of the Actris framework,
 first presented in the paper
 "Actris: Session Type Based Reasoning in Separation Logic".
@@ -46,9 +48,11 @@ The individual types contain the following:
 
 ## Notation
 
-The following table gives a mapping between the official notation in literature
+The following table gives a mapping between the notation in literature
 and the Coq mechanization:
 
+Dependent Separation Protocols:
+
 |        | Literature                    | Coq mechanization                     |
 |--------|-------------------------------|---------------------------------------|
 | Send   | `! x_1 .. x_n <v>{ P }. prot` | `<! x_1 .. x_n> MSG v {{ P }}; prot`  |
@@ -59,6 +63,17 @@ and the Coq mechanization:
 | Append | `prot_1 · prot_2`             | `prot_1 <++> prot_2`                  |
 | Dual   | An overlined protocol         | No notation                           |
 
+Semantic Session Types:
+
+|        | Literature                    | Coq mechanization                     |
+|--------|-------------------------------|---------------------------------------|
+| Send   | `!_{X_1 .. X_n} A . S`        | `<!! X_1 .. X_n> TY A ; S`            |
+| Recv   | `?_{X_1 .. X_n} A . S`        | `<?? X_1 .. X_n> TY A ; S`            |
+| End    | `end`                         | `END`                                 |
+| Select | `(+){ S_1 .. S_n }`           | `lty_choice SEND Ss`                  |
+| Branch | `&{ S_1 .. S_n }`             | `lty_choice RECV Ss`                  |
+| Dual   | An overlined protocol         | No notation                           |
+
 ## Coq tactics
 
 In order to prove programs using Actris, one can make use of a combination of
@@ -109,6 +124,7 @@ Concretely, the normalization performs the following actions:
 [ActrisProofMode]: theories/channel/proofmode.v
 
 ## Semantic Session Type System
+
 The logical relation for type safety of a semantic session type system is contained
 in the directory [theories/logrel](theories/logrel). The logical relation is
 defined across the following files:

papers/CONCUR20.md

+## Examples
+
+The parallel receive example in Section 4 can be found in
+  [theories/logrel/examples/double.v](../theories/logrel/examples/double.v):
+  This program performs two ``racy'' parallel receives on the same channel from two
+  different threads, using locks to allow the channel to be shared. This
+  program cannot be shown to be well-typed using the semantic typing rules.
+  Therefore, a manual proof of the well-typedness is given.
+
+The subprotocol assertion over two protocols that sends reference ownerships in
+Section 5 can be found in
+  [theories/examples/subprotocols.v](../theories/examples/subprotocols.v):
+  It contains the proof of the example.
+
+The recursive session subtyping example in Section 5 can be found in
+  [theories/logrel/examples/subtyping.v](../theories/logrel/examples/subtyping.v):