From e63c2a5c796e70d2a86b1ee4bd38c39105e2899a Mon Sep 17 00:00:00 2001
From: jihgfee <jihgfee@gmail.com>
Date: Wed, 23 Sep 2020 10:12:27 +0200
Subject: [PATCH] Referenced computation service example
---
papers/CPP21.md | 7 ++++++-
theories/logrel/examples/compute_service.v | 3 ++-
2 files changed, 8 insertions(+), 2 deletions(-)
diff --git a/papers/CPP21.md b/papers/CPP21.md
index 5767a03..c461674 100644
--- a/papers/CPP21.md
+++ b/papers/CPP21.md
@@ -15,7 +15,7 @@ contains an overview of the files in that directory.
Coq and the paper.
- The typing rule for branching (`ltyped_branch`) is written as a function
instead of an n-ary rule with multiple premises.
-- The disjunction of the compute client list invariant is encoded using a boolean
+- The disjunction of the compute client invariant is encoded using a boolean
flag, as it makes mechanisation easier.
- The mechanisation employs a typing judgement for values (`ltyped_val`),
for technical reasons. More details on this is found in
@@ -23,6 +23,10 @@ contains an overview of the files in that directory.
# Examples
+- The compute service example in Section 3 can be found in
+ [theories/logrel/examples/compute_service.v](../theories/logrel/examples/compute_service.v)
+ The program recursively receive computation requests, which it computes and
+ then send back. It is entirely type checked with the rules of the type system
- The parallel receive example in Section 4 can be found in
[theories/logrel/examples/par_recv.v](../theories/logrel/examples/par_recv.v):
This program performs two "racy" parallel receives on the same channel from
@@ -36,3 +40,4 @@ contains an overview of the files in that directory.
[theories/logrel/examples/compute_service.v](../theories/logrel/examples/compute_service.v).
The definition of the list type and the weakest precondition for `llength`
can be found in [theories/logrel/lib/list.v](../theories/logrel/lib/list.v)
+ It is type checked using a manual typing proof.
diff --git a/theories/logrel/examples/compute_service.v b/theories/logrel/examples/compute_service.v
index 79ac5fa..1495297 100644
--- a/theories/logrel/examples/compute_service.v
+++ b/theories/logrel/examples/compute_service.v
@@ -4,7 +4,8 @@
stop : end }
It recursively receives computations, computes them, and then
-sends back the results. *)
+sends back the results.
+The example is type checked using only the rules of the type system. *)
From iris.heap_lang Require Import metatheory.
From actris.channel Require Import proofmode.
From actris.logrel Require Import session_typing_rules.
--
GitLab