Commits · master · Iris / examples

Feb 16, 2024
- Patch now that frame ∃ looks beneath definitions again · a15d9e2e
  Ike Mulder authored 1 year ago
  
  a15d9e2e
Nov 06, 2023
- update dependencies · 2ebe30f2
  Ralf Jung authored 1 year ago
  
  2ebe30f2
May 03, 2023
- update dependencies · 259f1414
  Ralf Jung authored 2 years ago
  
  259f1414
May 02, 2023
- Build without warnings. · 5a3e6012
  Robbert Krebbers authored 2 years ago
  
  5a3e6012
Mar 09, 2023
- Bump Iris (beautify code for `iCombine .. gives`). · a64342ca
  Robbert Krebbers authored 2 years ago
  
  a64342ca
Sep 27, 2021
- bump Iris; adjust to f_equiv updates · 3e236ecc
  Ralf Jung authored 3 years ago
  
  3e236ecc
Jul 23, 2021
- make everything pass with coq-lint · d3599948
  Ralf Jung authored 3 years ago
  
  d3599948
- add missing explicit 'Global' · c612b471
  Ralf Jung authored 3 years ago
  
  c612b471
- concurrent_stacks: import Iris options · 64594a72
  Ralf Jung authored 3 years ago
  
  64594a72
Jun 03, 2021
- update dependencies · 2aec9ff3
  Ralf Jung authored 3 years ago
  
  2aec9ff3
Feb 16, 2021
- update dependencies · e380f7fe
  Ralf Jung authored 4 years ago
  
  e380f7fe
Feb 03, 2021
- avoid using Hoare triples · 0f8ce608
  Ralf Jung authored 4 years ago
  
  0f8ce608
Dec 18, 2020
- Bump Iris (persistent mapsto). · a8425b70
  Robbert Krebbers authored 4 years ago
  
  a8425b70
Dec 05, 2020
- remove a couple wp_fupd · fa1945be
  Ralf Jung authored 4 years ago
  
  fa1945be
Dec 04, 2020
- update Iris (wp_finish change) · 4177e16e
  Ralf Jung authored 4 years ago
  
  4177e16e
Jul 21, 2020
- Bump Iris (iExists ?). · ea96da9e
  Robbert Krebbers authored 4 years ago
  
  ea96da9e
Jun 18, 2020
- Add more discussion and fix some typos · 6ab998ef
  Ralf Jung authored 4 years ago
  
  6ab998ef
Sep 19, 2019
- Bump Iris. · 1813cb14
  Robbert Krebbers authored 5 years ago
  
  1813cb14
Jun 24, 2019
- bump Iris for CmpXchg change, and port everyting · 917d7705
  Ralf Jung authored 5 years ago
  
  917d7705
Jun 19, 2019
- bump Iris for comparison changes · d579dc8d
  Ralf Jung authored 5 years ago
  
  d579dc8d
Jun 18, 2019
- Bump Iris (C→O rename). · 06edc222
  Robbert Krebbers authored 5 years ago
  
  06edc222
Mar 06, 2019
- Restore comments · 14821493
  Daniel Gratzer authored 6 years ago
  
  14821493
Mar 05, 2019
- Small changes to specs, strengthen CAP spec · 9f47522f
  Daniel Gratzer authored 6 years ago
  
  9f47522f
Mar 04, 2019
- Added specs · 4cd40eb2
  Daniel Gratzer authored 6 years ago
  
  4cd40eb2
- Updated _CoqProject, updated concurrent_stacks to compile · 8a18cb8c
  Daniel Gratzer authored 6 years ago
  
  8a18cb8c
- New concurrent stack formalization · 65dcfa79
  Daniel Gratzer authored 6 years ago
  
  65dcfa79
Oct 31, 2018
- Update coq-iris : R2L evaluation, curry functions, Val constructor. · c18dc76f
  Jacques-Henri Jourdan authored 6 years ago
  
  c18dc76f
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: update to stronger CAS requirements · 77a45515
  Ralf Jung authored 6 years ago
  
  77a45515
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 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
Mar 07, 2018
- update concurrent_stack4 · 30b963ae
  Ralf Jung authored 7 years ago
  
  30b963ae
Feb 16, 2018
- concurrent stacks: add some comments · 82e114ce
  Ralf Jung authored 7 years ago
  
  82e114ce
Jan 12, 2018
- Add concurrent stacks with helping case study by Danny. · 5fc8c715
  Aleš Bizjak authored 7 years ago
  
  Fix #5.
  5fc8c715