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

link to TB readme

parent dc27a2ec
No related branches found
No related tags found
No related merge requests found
Pipeline #118852 passed
Hide whitespace changes
Inline Side-by-side
Showing
with 2 additions and 1 deletion
README.md
+ 2
− 1
View file @ 003179e0
# Simuliris Coq development # Simuliris Coq development
This repository contains the Coq development of Simuliris (paper presented at POPL22: https://iris-project.org/pdfs/2022-popl-simuliris.pdf). This repository contains the Coq development of Simuliris (paper presented at POPL22: https://iris-project.org/pdfs/2022-popl-simuliris.pdf).
It also contains the proofs for [Tree Borrows](theories/tree_borrows/README.md).
## Prerequisites ## Prerequisites
...@@ -65,7 +66,7 @@ The project follows the following structure below the `theories` folder: ...@@ -65,7 +66,7 @@ The project follows the following structure below the `theories` folder:
* `adequacy.v` contains the resulting adequacy proof. * `adequacy.v` contains the resulting adequacy proof.
* `examples` contains example optimizations, see below. * `examples` contains example optimizations, see below.
- `tree_borrows` contains the Simuliris development of Tree Borrows. - `tree_borrows` contains the Simuliris development of Tree Borrows.
This development has its own README in `tree_borrows/README.md`. This development has its [own README](theories/tree_borrows/README.md).
## Theorems, definitions, and examples referenced in the paper ## Theorems, definitions, and examples referenced in the paper
......
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