Commits · a438921d1e81805a694099e68dc89bc213c42c42 · Iris / Fairis · GitLab

12 Feb, 2018 1 commit
- Update to use new ElimModal from Robbert; remove %I delimiter from upred to avoid conflict with bi. · a438921d
  Joseph Tassarotti authored Feb 12, 2018
  
  a438921d
11 Feb, 2018 2 commits
- WIP getting pviewshifts to work correctly with iMod tactic. · 08ee7373
  Joseph Tassarotti authored Feb 11, 2018
  
  08ee7373
- Update for dependencies; fix ownership (except unresolved issue of ATimeless... · 8e793079
  Joseph Tassarotti authored Feb 11, 2018
```
Update for dependencies; fix ownership (except unresolved issue of ATimeless and some other modality interactions).
```
  8e793079
16 Jan, 2018 1 commit
- Define BI structure; admits for things involving 'plainly' as they are supposed to be removed. · 5a8e79e8
  Joseph Tassarotti authored Jan 15, 2018
  
  5a8e79e8
15 Jan, 2018 1 commit
- Bump stdpp and proofmode. · 89425063
  Joseph Tassarotti authored Jan 15, 2018
  
  89425063
05 Dec, 2017 2 commits
- Import iris versions of ofe.v and cofe_solver.v · 058a6f69
  Joseph Tassarotti authored Dec 05, 2017
  
  058a6f69
- Add proof mode dependency to opam. · 17928602
  Joseph Tassarotti authored Dec 05, 2017
  
  17928602
04 Dec, 2017 6 commits
- Fix some aspects of readme. · d21adae8
  Joseph Tassarotti authored Dec 04, 2017
  
  d21adae8
- Change readme page title · 8e7da16d
  Joseph Tassarotti authored Dec 04, 2017
  
  8e7da16d
- Update to modern coq directory structure; rename project to 'fri', set up opam. · baeeaebd
  Joseph Tassarotti authored Dec 04, 2017
  
  baeeaebd
- Merge branch 'fair-refine' into fair-refine-stdpp · b53c8c7b
  Joseph Tassarotti authored Dec 04, 2017
  
  b53c8c7b
- Update readme for dependencies; remove verbose tactics. · 3a451d4f
  Joseph Tassarotti authored Dec 04, 2017
  
  3a451d4f
- Delete the unneed prelude/ stuff that was a duplication of old coq-stdpp. · 0210a602
  Joseph Tassarotti authored Dec 04, 2017
  
  0210a602
03 Dec, 2017 1 commit
- Finish fixing old proofs; delete unused array_lang/ stuff. Performance is still very bad. · f6101454
  Joseph Tassarotti authored Dec 03, 2017
  
  f6101454
02 Dec, 2017 2 commits
- WIP. · c8bb5f4a
  Joseph Tassarotti authored Dec 02, 2017
  
  c8bb5f4a
- Update up through heap_lang. · 145afd4d
  Joseph Tassarotti authored Dec 02, 2017
  
  145afd4d
01 Dec, 2017 3 commits
- Switched back to having ucmra with discrete unit; more WIP updating. · 825e7e74
  Joseph Tassarotti authored Dec 01, 2017
  
  825e7e74
- Fix bug in old proofmode; I think I need ucmra to have discrete units again. · df6f2669
  Joseph Tassarotti authored Dec 01, 2017
  
  df6f2669
- Continuing w/ replacement with ofes and stdpp; hitting bugs in old proofmode... · 85ca3e31
  Joseph Tassarotti authored Dec 01, 2017
```
Continuing w/ replacement with ofes and stdpp; hitting bugs in old proofmode after change -- not sure whether to fix.
```
  85ca3e31
30 Nov, 2017 3 commits
- WIP switching to stdpp and moving from Cofe to Ofe. · aebbe02a
  Joseph Tassarotti authored Nov 30, 2017
  
  aebbe02a
- Merge branch 'fair-refine-8.7' into fair-refine · 1b5e31d9
  Joseph Tassarotti authored Nov 30, 2017
  
  1b5e31d9
- Update to 8.7. · 18990e66
  Joseph Tassarotti authored Nov 30, 2017
  
  18990e66
22 Oct, 2016 1 commit
- Update Coq outline. · bdcddb9c
  Joseph Tassarotti authored Oct 21, 2016
  
  bdcddb9c
08 Oct, 2016 2 commits
- Re-name; update readme. · d63b5243
  Joseph Tassarotti authored Oct 08, 2016
  
  d63b5243
- Soundness of logical relation and closed proof of refinement for ticket -> clh example. · acde4085
  Joseph Tassarotti authored Oct 08, 2016
  
  acde4085
07 Oct, 2016 1 commit
- Finish fundamental lemma for lock refinement. · cba39706
  Joseph Tassarotti authored Oct 07, 2016
  
  cba39706
06 Oct, 2016 1 commit
- WIP logical relation for lock refinement. · 382fde26
  Joseph Tassarotti authored Oct 06, 2016
  
  382fde26
05 Oct, 2016 2 commits
- WIP fundamental lemma for lock refinement. · 9074f85c
  Joseph Tassarotti authored Oct 05, 2016
  
  9074f85c
- Define generic logical relation for proving refinements for locks. · 87d689a5
  Joseph Tassarotti authored Oct 05, 2016
  
  87d689a5
04 Oct, 2016 5 commits
- Some clean-up. · c3d009b0
  Joseph Tassarotti authored Oct 04, 2016
  
  c3d009b0
- Remove remaining superfluous skip from CLH · 51fd5745
  Joseph Tassarotti authored Oct 04, 2016
  
  51fd5745
- Proof-rule for multi-steps of heap lang source; Remove extra skip from CLH · 4cf25eea
  Joseph Tassarotti authored Oct 04, 2016
  
  4cf25eea
- Clean-up ticket_clh file. · d774c630
  Joseph Tassarotti authored Oct 04, 2016
  
  d774c630
- Fix solve_atomic, fix clh release code; prove refinement triple for release · fe261bca
  Joseph Tassarotti authored Oct 04, 2016
  
  fe261bca
03 Oct, 2016 2 commits
- Extend lock refinement proof spec so that you can protect some affine resource R · 5764c90e
  Joseph Tassarotti authored Oct 03, 2016
  
  5764c90e
- Missing files from last commit; Finish acquire triple. · 2aa6d846
  Joseph Tassarotti authored Oct 03, 2016
  
  2aa6d846
01 Oct, 2016 1 commit
- Fixes to tactics; Fix code of clh; WIP refinement proof for ticket -> clh. · ba3eee94
  Joseph Tassarotti authored Oct 01, 2016
  
  ba3eee94
25 Sep, 2016 2 commits
- Add CLH and Ticket lock implementations. · 39e71a35
  Joseph Tassarotti authored Sep 25, 2016
  
  39e71a35
- Add Swap and FAI primitives to heap lang w/ tactic support. · 1590ce5d
  Joseph Tassarotti authored Sep 25, 2016
  
  1590ce5d
24 Sep, 2016 1 commit
- Add support for delay steps when using heap lang as source lang. · c00a0578
  Joseph Tassarotti authored Sep 24, 2016
  
  c00a0578