Commits · b9e2293334aa8ade18cb8c2a7e041cafa766dd26 · Paolo G. Giarrusso / examples

Sep 30, 2018
- write URLs the way opam writes them · b9e22933
  Ralf Jung authored 6 years ago
  
  b9e22933
Sep 19, 2018
- use Docker image matching CI branch · 81d56417
  Ralf Jung authored 6 years ago
  
  81d56417
Sep 18, 2018
- update CI for opam 2 · 9f14f4f8
  Ralf Jung authored 6 years ago
  
  9f14f4f8
Jul 13, 2018
- fix for Coq 8.7 · 45797729
  Ralf Jung authored 6 years ago
  
  45797729
- Merge branch 'logatom_stack' into 'master' · 65e38263
  Ralf Jung authored 6 years ago
  
  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 6 years ago
  
  7c7bc060
- prove stack pop; add general stack interface · 1835a90a
  Ralf Jung authored 6 years ago
  
  1835a90a
- prove stack push · 98ee891b
  Ralf Jung authored 6 years ago
  
  98ee891b
- define the protocol and prove the constructor · 8ed6910d
  Ralf Jung authored 6 years ago
  
  8ed6910d
- Start with logically atomic stack: Write the code · 43199eff
  Ralf Jung authored 6 years ago
  
  43199eff
- bump Iris to master · f6521223
  Ralf Jung authored 6 years ago
  
  f6521223
Jul 05, 2018
- concurrent stacks: also unify concurrent bag (per-element) specs for stacks 1 and 2 · 0247cec5
  Ralf Jung authored 6 years ago
  
  0247cec5
Jul 04, 2018
- bump Iris · 68473b43
  Ralf Jung authored 6 years ago
  
  68473b43
- bump Iris (for new pm_reduce) · 90fdd99e
  Ralf Jung authored 6 years ago
  
  90fdd99e
- bump Iris: update to stronger CAS requirements · 77a45515
  Ralf Jung authored 6 years ago
  
  77a45515
Jun 28, 2018
- bump Iris · 2645095c
  Ralf Jung authored 6 years ago
  
  2645095c
Jun 23, 2018
- port to gen_proofmode · 791a505d
  Ralf Jung authored 6 years ago
  
  791a505d
- bump Iris; fix for std++ change · 3aa2c6c8
  Ralf Jung authored 6 years ago
  
  3aa2c6c8
Jun 22, 2018
- update CI · b6f3e75d
  Ralf Jung authored 6 years ago
  
  b6f3e75d
- nightly builds: use latest std++ · fe93dc05
  Ralf Jung authored 6 years ago
  
  fe93dc05
Jun 21, 2018
- update Makefile and CI · 0c66274b
  Ralf Jung authored 6 years ago
  
  0c66274b
Jun 20, 2018
- Use `iAsimpl` more widely. · e9cfcda6
  Robbert Krebbers authored 6 years ago and Ralf Jung committed 6 years ago
  
  e9cfcda6
- Hackish `iAsimpl` that runs `asimpl` selectively. · 45fa0a9c
  Robbert Krebbers authored 6 years ago and Ralf Jung committed 6 years ago
  
  TODO: use it more widely if this indeed improves performance.
  45fa0a9c
- fix build · 226181b6
  Ralf Jung authored 6 years ago
  
  226181b6
- add hocap target · c34a636b
  Ralf Jung authored 6 years ago
  
  c34a636b
- Merge branch 'hocap' into 'master' · 18c334bc
  Ralf Jung authored 6 years ago
  
  Implement modular specifications from the HOCAP paper See merge request FP/iris-examples!5
  18c334bc
Jun 14, 2018
- fix build · feae9588
  Ralf Jung authored 6 years ago
  
  feae9588
- concurrent stacks: add an interface that both stack3 and stack4 implement · 2649cb67
  Ralf Jung authored 6 years ago
  
  Had to slightly tweak (strengthen) stack3's spec for that
  2649cb67
Jun 12, 2018
- add attributions to the README · 3ca1fa65
  Ralf Jung authored 6 years ago
  
  3ca1fa65
- dang I screwed up the timing_conf · 3d5498b7
  Ralf Jung authored 6 years ago
  
  3d5498b7
- do timing on Coq 8.8 · 93748a54
  Ralf Jung authored 6 years ago
  
  93748a54
Jun 04, 2018
- .gitignore · f9bee86a
  Ralf Jung authored 6 years ago
  
  f9bee86a
May 20, 2018
- bump iris; small rename fix needed · d4c7170c
  Ralf Jung authored 6 years ago
  
  d4c7170c
May 10, 2018
- README tweaks · 3d9137d6
  Dan Frumin authored 6 years ago
  
  3d9137d6
- Make parfib.v compile with the latest Iris version · fa9bc158
  Dan Frumin authored 6 years ago
  
  fa9bc158
- Explain the circularity in concurrent_runners.v · d086103b
  Dan Frumin authored 6 years ago
  
  d086103b
- Bag with contributions · 62dd285f
  Dan Frumin authored 6 years ago
  
  62dd285f
- Update comments · a1c9f69a
  Dan Frumin authored 6 years ago
  
  a1c9f69a
- isRunner -> runner · bc082bf8
  Dan Frumin authored 6 years ago
  
  bc082bf8
- Move oneshot RA to a separate module · 6c2c6343
  Dan Frumin authored 6 years ago
  
  6c2c6343