From ee3c6ec10331ced77c3a19cc04f10b693767997a Mon Sep 17 00:00:00 2001
From: Robbert Krebbers
Date: Mon, 25 Nov 2019 13:09:06 +0100
Subject: [PATCH] More README tweaking.
---
README.md | 6 +++---
1 file changed, 3 insertions(+), 3 deletions(-)
diff --git a/README.md b/README.md
index dc253bc..b755561 100644
--- a/README.md
+++ b/README.md
@@ -45,8 +45,8 @@ correspond to the following parts of the paper:
## Notation
-The notation for Dependent Separation Protocols differ between the paper and
-the Coq mechanization:
+The following table gives a mapping between the notation in the paper and the
+Coq mechanization:
| | Paper | Coq mechanization |
|--------|-------------------------------|---------------------------------------|
@@ -175,7 +175,7 @@ of Actris and the formalization in Coq, that are briefly discussed here.
later modalities expose that these operations perform at least three steps in
the operational semantics, and are needed to deal with the three levels of
indirection in the invariant for protocols:
- 1. the `▶` in the CPS encoding of protocols,
+ 1. the `▶` in the model of protocols,
2. the higher-order ghost state used for ownership of protocols, and
3. the opening of the protocol invariant.
--
2.26.2