Commit 0d1f1e52 authored by Robbert Krebbers's avatar Robbert Krebbers

More links in README.

parent 8a8a3394
Pipeline #2752 passed with stage
in 9 minutes and 31 seconds
...@@ -28,27 +28,27 @@ running: ...@@ -28,27 +28,27 @@ running:
## Structure ## Structure
* The folder `prelude` contains an extended "Standard Library" by Robbert * The folder [prelude](prelude) contains an extended "Standard Library" by
Krebbers <http://robbertkrebbers.nl/thesis.html>. Robbert Krebbers <http://robbertkrebbers.nl/thesis.html>.
* The folder `algebra` contains the COFE and CMRA constructions as well as * The folder [algebra](algebra) contains the COFE and CMRA constructions as well
the solver for recursive domain equations. as the solver for recursive domain equations.
* The folder `program_logic` builds the semantic domain of Iris, defines and * The folder [program_logic](program_logic) builds the semantic domain of Iris,
verifies primitive view shifts and weakest preconditions, and builds some defines and verifies primitive view shifts and weakest preconditions, and
language-independent derived constructions (e.g., STSs). builds some language-independent derived constructions (e.g., STSs).
* The folder `heap_lang` defines the ML-like concurrent heap language * The folder [heap_lang](heap_lang) defines the ML-like concurrent heap language
* The subfolder `lib` contains a few derived constructions within this * The subfolder [lib](heap_lang/lib) contains a few derived constructions
language, e.g., parallel composition. within this language, e.g., parallel composition.
Most notable here s `lib/barrier`, the implementation and proof of a barrier Most notable here s [lib/barrier](heap_lang/lib/barrier), the implementation
as described in <http://doi.acm.org/10.1145/2818638>. and proof of a barrier as described in <http://doi.acm.org/10.1145/2818638>.
* The folder `proofmode` contains the Iris proof mode, which extends Coq with * The folder [proofmode](proofmode) contains the Iris proof mode, which extends
contexts for persistent and spatial Iris assertions. It also contains tactics Coq with contexts for persistent and spatial Iris assertions. It also contains
for interactive proofs in Iris. Documentation can be found in tactics for interactive proofs in Iris. Documentation can be found in
[`ProofMode.md`](ProofMode.md). [ProofMode.md](ProofMode.md).
* The folder `tests` contains modules we use to test our infrastructure. * The folder [tests](tests) contains modules we use to test our infrastructure.
Users of the Iris Coq library should *not* depend on these modules; they may Users of the Iris Coq library should *not* depend on these modules; they may
change or disappear without any notice. change or disappear without any notice.
## Documentation ## Documentation
A LaTeX version of the core logic definitions and some derived forms is A LaTeX version of the core logic definitions and some derived forms is
available in [`docs/iris.tex`](docs/iris.tex). available in [docs/iris.tex](docs/iris.tex).
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