Skip to content

GitLab

Commit 9064e78f authored by Ralf Jung's avatar Ralf Jung
Browse files

README: add link to MoSeL paper website

parent a7de5f7b
Hide whitespace changes
Inline Side-by-side
README.md
View file @ 9064e78f
...@@ -73,9 +73,10 @@ followed by `make build-dep`. ...@@ -73,9 +73,10 @@ followed by `make build-dep`.
constructions that work for any such language. constructions that work for any such language.
* The folder [bi](theories/bi) contains the BI++ laws, as well as derived * The folder [bi](theories/bi) contains the BI++ laws, as well as derived
connectives, laws and constructions that are applicable for general BIS. connectives, laws and constructions that are applicable for general BIS.
* The folder [proofmode](theories/proofmode) contains MoSeL, which extends Coq * The folder [proofmode](theories/proofmode) contains
with contexts for intuitionistic and spatial BI++ assertions. It also contains [MoSeL](http://iris-project.org/mosel/), which extends Coq with contexts for
tactics for interactive proofs. Documentation can be found in intuitionistic and spatial BI++ assertions. It also contains tactics for
interactive proofs. Documentation can be found in
[ProofMode.md](ProofMode.md). [ProofMode.md](ProofMode.md).
* The folder [heap_lang](theories/heap_lang) defines the ML-like concurrent heap * The folder [heap_lang](theories/heap_lang) defines the ML-like concurrent heap
language language
......
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