Skip to content
Snippets Groups Projects
Commit b5e3e5a2 authored by Yusuke Matsushita's avatar Yusuke Matsushita
Browse files

Minor edit of README.md

parent 5f5dd7bc
No related branches found
No related tags found
No related merge requests found
Pipeline #64122 passed
......@@ -61,10 +61,11 @@ followed by `make build-dep`.
## Where to Find the Proof Rules From the Paper
The derived rules mentioned in the paper can be found [here](theories/typing/examples/derived_rules.v).
### Type System Rules
### Type System Rules --- from the RustBelt Paper
The files in [typing](theories/typing) prove semantic versions of the proof
rules given in the (RustBelt) paper. Notice that mutable borrows are called
rules given in the *RustBelt* paper. Notice that mutable borrows are called
"unique borrows" in the Coq development.
| Proof Rule | File | Lemma |
......
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