Commit a9756949 authored by Robbert's avatar Robbert

Update README.md

parent 6a63de9e
...@@ -9,6 +9,7 @@ Aleš Bizjak, Daniel Gratzer, Robbert Krebbers, and Lars Birkedal. ...@@ -9,6 +9,7 @@ Aleš Bizjak, Daniel Gratzer, Robbert Krebbers, and Lars Birkedal.
Iron has been built and tested with the following dependencies Iron has been built and tested with the following dependencies
- Coq 8.7.1 / 8.7.2 / 8.8.0 - 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) - A development version of [std++](https://gitlab.mpi-sws.org/iris/stdpp)
## Directory Structure ## Directory Structure
...@@ -23,7 +24,7 @@ Iron has been built and tested with the following dependencies ...@@ -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 - The semantics of the connectives of the lifted logic are given in
`theories/bi/fracpred.v`. `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 logic but instead contains the definitions of ∧, ∗, ∀, and other
the other connectives. It also contains all the rules of the the other connectives. It also contains all the rules of the
specific to this logic that are used later. specific to this logic that are used later.
...@@ -34,7 +35,6 @@ Iron has been built and tested with the following dependencies ...@@ -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 `theories/iron_logic` much of the core Iron logic discussed
in Section 2 is defined. in Section 2 is defined.
* Uniformity with respect to fractions is defined in * Uniformity with respect to fractions is defined in
`theories/iron_logic/iron.v` as `Uniform` and `theories/iron_logic/iron.v` as `Uniform` and
several closure properties of it are proved. several closure properties of it are proved.
...@@ -45,7 +45,6 @@ Iron has been built and tested with the following dependencies ...@@ -45,7 +45,6 @@ Iron has been built and tested with the following dependencies
- The formalization specific to the λref,conc is in - The formalization specific to the λref,conc is in
`theories/heap_lang`. `theories/heap_lang`.
* The definition of the heap in terms of ghost state from Section * 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 5 is in `theories/heap_lang/heap.v` as `heapG`. So too are
the definitions of ↦ and e (in the formalization called `perm`). the definitions of ↦ and e (in the formalization called `perm`).
...@@ -66,17 +65,16 @@ Iron has been built and tested with the following dependencies ...@@ -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 the proofs and no significant bookkeeping beyond what is found in
vanilla Iris. 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 formalized in the lifted logic but in the formalization this is
factored out into `spawn` in `theories/heap_lang/lib/spawn.v`. 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.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.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.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.4 is in `theories/heap_lang/lib/message_passing_example.v`.
* The example from 3.5 is in `theories/heap_lang/lib/par.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 use the same state transition system (from Figure 3). This is formalized in
`theories/heap_lang/lib/transfer_resource_sts.v`. `theories/heap_lang/lib/transfer_resource_sts.v`.
......
Markdown is supported
0%
or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment