From 03d3465f8d79df3b299240bc6e0840165b5d746d Mon Sep 17 00:00:00 2001
From: Jonas Kastberg <jihgfee@gmail.com>
Date: Sun, 10 May 2020 12:37:02 +0200
Subject: [PATCH] Concur2020
---
README.md | 18 +++++++++++++++++-
papers/CONCUR20.md | 16 ++++++++++++++++
2 files changed, 33 insertions(+), 1 deletion(-)
create mode 100644 papers/CONCUR20.md
diff --git a/README.md b/README.md
index 64a999f..645f061 100644
--- a/README.md
+++ b/README.md
@@ -1,5 +1,7 @@
# 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:
diff --git a/papers/CONCUR20.md b/papers/CONCUR20.md
new file mode 100644
index 0000000..ae23ea2
--- /dev/null
+++ b/papers/CONCUR20.md
@@ -0,0 +1,16 @@
+## 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):
--
GitLab