From a97569497e62b43cd6779c5493fba0e226c646b4 Mon Sep 17 00:00:00 2001 From: Robbert Date: Wed, 31 Oct 2018 20:34:01 +0100 Subject: [PATCH] Update README.md --- README.md | 10 ++++------ 1 file changed, 4 insertions(+), 6 deletions(-) diff --git a/README.md b/README.md index 0a59f1e..93f3086 100644 --- a/README.md +++ b/README.md @@ -9,6 +9,7 @@ Aleš Bizjak, Daniel Gratzer, Robbert Krebbers, and Lars Birkedal. Iron has been built and tested with the following dependencies - Coq 8.7.1 / 8.7.2 / 8.8.0 + - A development version of [Iris](https://gitlab.mpi-sws.org/FP/iris-coq) - A development version of [std++](https://gitlab.mpi-sws.org/iris/stdpp) ## Directory Structure @@ -23,7 +24,7 @@ Iron has been built and tested with the following dependencies - The semantics of the connectives of the lifted logic are given in `theories/bi/fracpred.v`. - This file does not contain a description of the lifted program + This file does not contain a description of the lifted program logic but instead contains the definitions of ∧, ∗, ∀, and other the other connectives. It also contains all the rules of the specific to this logic that are used later. @@ -34,7 +35,6 @@ Iron has been built and tested with the following dependencies - In `theories/iron_logic` much of the core Iron logic discussed in Section 2 is defined. - * Uniformity with respect to fractions is defined in `theories/iron_logic/iron.v` as `Uniform` and several closure properties of it are proved. @@ -45,7 +45,6 @@ Iron has been built and tested with the following dependencies - The formalization specific to the λref,conc is in `theories/heap_lang`. - * The definition of the heap in terms of ghost state from Section 5 is in `theories/heap_lang/heap.v` as `heapG`. So too are the definitions of ↦ and e (in the formalization called `perm`). @@ -66,17 +65,16 @@ Iron has been built and tested with the following dependencies the proofs and no significant bookkeeping beyond what is found in vanilla Iris. - As mentioned in the paper, a small portion of `par` cannot be + As mentioned in the paper, a small portion of `par` cannot be formalized in the lifted logic but in the formalization this is factored out into `spawn` in `theories/heap_lang/lib/spawn.v`. - * The example from 3.1 is in `theories/heap_lang/lib/resource_transfer_par.v`. * The example from 3.2 is in `theories/heap_lang/lib/resource_transfer_fork.v`. * The example from 3.3 is in `theories/heap_lang/lib/message_passing.v`. * The example from 3.4 is in `theories/heap_lang/lib/message_passing_example.v`. * The example from 3.5 is in `theories/heap_lang/lib/par.v`. - Note that `spawn.v`, `resource_transfer_par.v`, and `resource_transfer_fork.v` + Note that `spawn.v`, `resource_transfer_par.v`, and `resource_transfer_fork.v` use the same state transition system (from Figure 3). This is formalized in `theories/heap_lang/lib/transfer_resource_sts.v`. -- 2.26.2