Commit ff1475f1 authored by Hai Dang's avatar Hai Dang

Update README.md

parent 13c7f81d
......@@ -48,7 +48,7 @@ The Coq development is in folder [coq/ra/](coq/ra).
| 2.3 | $`\lambda_{RN}`$ language | `expr` (expressions) and `step` (reductions) | [lang.v](coq/ra/lang.v) |
| 3.2.1 | Base logic local assertions and invariants | `Seen` `Hist` `HInv` `PSInv` | [base/ghosts.v](coq/ra/base/ghosts.v) |
| 3.2.1 | Base logic NA rules | `f_read_na` `f_write_na` `f_alloc` `f_dealloc` | [base](coq/ra/base)/na_*.v [base/alloc.v](coq/ra/base/alloc.v) [base/dealloc.v](coq/ra/base/dealloc.v) |
| 3.2.2 | Message Passing in the base logic | `message_passing_base_spec` | [example/message_passing_base.v](coq/ra/example/message_passing_base.v) |
| 3.2.2 | Message Passing in the base logic | `message_passing_base_spec` | [examples/message_passing_base.v](coq/ra/examples/message_passing_base.v) |
| 4.1 | iGPS NA rules | `na_read` `na_write`; **fractional versions**: `na_read_frac` `na_write_frac` | [na.v](coq/ra/na.v) |
| 4.1 | iGPS normal (*plain*) protocol rules | `GPS_PP_*` lemmas | [gps/plain.v](coq/ra/gps/plain.v) |
| 4.1, Appendix C | iGPS escrows and exchanges | `exchange_*` and `escrows_*` lemmas | [escrows.v](coq/ra/escrows.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