README.txt 1.12 KB
Newer Older
Ralf Jung's avatar
Ralf Jung committed
1 2 3 4 5 6 7 8 9 10 11 12
This folder contains the Coq development for
Iris: Monoids and Invariants as an Orthogonal Basis for Concurrent Reasoning
Ralf Jung <>
David Swasey <>
Filip Sieczkowski <>
Kasper Svendsen <>
Aaron Turon <>
Lars Birkedal <>
Derek Dreyer <>

Ralf Jung's avatar
Ralf Jung committed
13 14 15 16 17 18 19 20 21
It uses a Coq library in lib/ by Sieczkowski et al. to solve the recursive domain equation (see the paper for a reference).

This folder is organized as follows:
* core_lang.v contains the axioms about the language
* lang.v defines the threadpool reduction and derives some lemmas from core_lang.v
* masks.v introduces some lemmas about masks
* world_prop.v uses the aforementioned Coq library to construct the domain for Iris propositions
* iris.v is the main file and contains the actual logic and the proof of the rules for view shifts and Hoare tiples

Ralf Jung's avatar
Ralf Jung committed
Run "make" in this folder to build it all.
Ralf Jung's avatar
Ralf Jung committed
23 24
Be aware that iris.v takes a long time to check and needs significant amounts of RAM!
8GiB may be sufficient, but to be safe you should have 16GiB and give it around 2 to 3 hours.