Skip to content
Snippets Groups Projects
Commit 227e5403 authored by Ralf Jung's avatar Ralf Jung
Browse files

update readme

parent 78ee0888
No related branches found
No related tags found
No related merge requests found
Pipeline #93099 passed
......@@ -37,7 +37,7 @@ The individual types contain the following:
bidirectional channels in terms of Iris's HeapLang language, with specifications
defined in terms of the dependent separation protocols.
The relevant definitions and proof rules are as follows:
+ `iProto_mapsto`: endpoint ownership (notation `↣`).
+ `iProto_pointsto`: endpoint ownership (notation `↣`).
+ `new_chan_spec`, `send_spec` and `recv_spec`: proof rule for `new_chan`,
`send`, and `recv`.
+ `select_spec` and `branch_spec`: proof rule for the derived (binary)
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment