Commits · 34b978b526364b3fe44e14f22f20ffabc4f936c8 · Iris / examples

07 Oct, 2018 1 commit
- Fix opam. · 34b978b5
  Robbert Krebbers authored Oct 07, 2018
  
  34b978b5
06 Oct, 2018 1 commit
- Bump Iris. · 778406b2
  Robbert Krebbers authored Oct 06, 2018
  
  778406b2
30 Sep, 2018 1 commit
- write URLs the way opam writes them · b9e22933
  Ralf Jung authored Sep 30, 2018
  
  b9e22933
19 Sep, 2018 1 commit
- use Docker image matching CI branch · 81d56417
  Ralf Jung authored Sep 19, 2018
  
  81d56417
18 Sep, 2018 1 commit
- update CI for opam 2 · 9f14f4f8
  Ralf Jung authored Sep 18, 2018
  
  9f14f4f8
13 Jul, 2018 8 commits
- fix for Coq 8.7 · 45797729
  Ralf Jung authored Jul 13, 2018
  
  45797729
- Merge branch 'logatom_stack' into 'master' · 65e38263
  Ralf Jung authored Jul 13, 2018
```
Logically atomic stack

See merge request FP/iris-examples!9
```
  65e38263
- add abstract HoCAP-style spec and show that it implies the logically atomic one · 7c7bc060
  Ralf Jung authored Jun 18, 2018
  
  7c7bc060
- prove stack pop; add general stack interface · 1835a90a
  Ralf Jung authored Jun 13, 2018
  
  1835a90a
- prove stack push · 98ee891b
  Ralf Jung authored Jun 13, 2018
  
  98ee891b
- define the protocol and prove the constructor · 8ed6910d
  Ralf Jung authored Jun 13, 2018
  
  8ed6910d
- Start with logically atomic stack: Write the code · 43199eff
  Ralf Jung authored Jun 12, 2018
  
  43199eff
- bump Iris to master · f6521223
  Ralf Jung authored Jul 13, 2018
  
  f6521223
05 Jul, 2018 1 commit
- concurrent stacks: also unify concurrent bag (per-element) specs for stacks 1 and 2 · 0247cec5
  Ralf Jung authored Jul 06, 2018
  
  0247cec5
04 Jul, 2018 3 commits
- bump Iris · 68473b43
  Ralf Jung authored Jul 04, 2018
  
  68473b43
- bump Iris (for new pm_reduce) · 90fdd99e
  Ralf Jung authored Jul 04, 2018
  
  90fdd99e
- bump Iris: update to stronger CAS requirements · 77a45515
  Ralf Jung authored Jul 04, 2018
  
  77a45515
28 Jun, 2018 1 commit
- bump Iris · 2645095c
  Ralf Jung authored Jun 28, 2018
  
  2645095c
23 Jun, 2018 2 commits
- port to gen_proofmode · 791a505d
  Ralf Jung authored Jun 21, 2018
  
  791a505d
- bump Iris; fix for std++ change · 3aa2c6c8
  Ralf Jung authored Jun 23, 2018
  
  3aa2c6c8
22 Jun, 2018 2 commits
- update CI · b6f3e75d
  Ralf Jung authored Jun 23, 2018
  
  b6f3e75d
- nightly builds: use latest std++ · fe93dc05
  Ralf Jung authored Jun 22, 2018
  
  fe93dc05
21 Jun, 2018 1 commit
- update Makefile and CI · 0c66274b
  Ralf Jung authored Jun 21, 2018
  
  0c66274b
20 Jun, 2018 5 commits
- Use `iAsimpl` more widely. · e9cfcda6
  Robbert Krebbers authored Jun 16, 2018
  
  e9cfcda6
- Hackish `iAsimpl` that runs `asimpl` selectively. · 45fa0a9c
  Robbert Krebbers authored Jun 16, 2018
```
TODO: use it more widely if this indeed improves performance.
```
  45fa0a9c
- fix build · 226181b6
  Ralf Jung authored Jun 20, 2018
  
  226181b6
- add hocap target · c34a636b
  Ralf Jung authored Jun 20, 2018
  
  c34a636b
- Merge branch 'hocap' into 'master' · 18c334bc
  Ralf Jung authored Jun 20, 2018
```
Implement modular specifications from the HOCAP paper

See merge request FP/iris-examples!5
```
  18c334bc
14 Jun, 2018 2 commits
- fix build · feae9588
  Ralf Jung authored Jun 14, 2018
  
  feae9588
- concurrent stacks: add an interface that both stack3 and stack4 implement · 2649cb67
  Ralf Jung authored Jun 14, 2018
```
Had to slightly tweak (strengthen) stack3's spec for that
```
  2649cb67
12 Jun, 2018 3 commits
- add attributions to the README · 3ca1fa65
  Ralf Jung authored Jun 12, 2018
  
  3ca1fa65
- dang I screwed up the timing_conf · 3d5498b7
  Ralf Jung authored Jun 12, 2018
  
  3d5498b7
- do timing on Coq 8.8 · 93748a54
  Ralf Jung authored Jun 12, 2018
  
  93748a54
04 Jun, 2018 1 commit
- .gitignore · f9bee86a
  Ralf Jung authored Jun 04, 2018
  
  f9bee86a
20 May, 2018 1 commit
- bump iris; small rename fix needed · d4c7170c
  Ralf Jung authored May 20, 2018
  
  d4c7170c
10 May, 2018 5 commits
- README tweaks · 3d9137d6
  Dan Frumin authored May 10, 2018
  
  3d9137d6
- Make parfib.v compile with the latest Iris version · fa9bc158
  Dan Frumin authored Apr 30, 2018
  
  fa9bc158
- Explain the circularity in concurrent_runners.v · d086103b
  Dan Frumin authored Apr 15, 2018
  
  d086103b
- Bag with contributions · 62dd285f
  Dan Frumin authored Apr 10, 2018
  
  62dd285f
- Update comments · a1c9f69a
  Dan Frumin authored Apr 10, 2018
  
  a1c9f69a