Commits · master · Iris / ITree Program Logic

Mar 03, 2025
- Update Iris version. · 0876c9cd
  Max Vistrup authored 3 months ago
  
  0876c9cd
Nov 27, 2024
- mention affiliation in copyright · a145f273
  Ralf Jung authored 6 months ago
  
  a145f273
Nov 21, 2024
- fix some footnote references · 6684c37d
  Ralf Jung authored 6 months ago
  
  6684c37d
- fix markdown · 95cccb16
  Ralf Jung authored 6 months ago
  
  95cccb16
- make more things links · 90f7b72a
  Ralf Jung authored 6 months ago
  
  90f7b72a
- make readme link to paper website · 99a86c1c
  Ralf Jung authored 6 months ago
  
  99a86c1c
Nov 20, 2024
- Merge branch 'master' of https://gitlab.mpi-sws.org/iris/itree-program-logic · 3e466c6a
  Max Vistrup authored 6 months ago
  
  3e466c6a
- enable CI here · 528554ce
  Ralf Jung authored 6 months ago
  
  528554ce
- Add Coq/paper mapping. · cc4bfeb9
  Max Vistrup authored 6 months ago
  
  cc4bfeb9
- remove leftover files · 5fcc4d4e
  Ralf Jung authored 6 months ago
  
  5fcc4d4e
Nov 18, 2024
- Merge branch 'master' of gitlab.inf.ethz.ch:ou-plf/iris-itree · 701268e1
  Max Vistrup authored 6 months ago
  
  701268e1
Nov 08, 2024
- Update ExampleLang formalization to paper. · 4398f998
  Max Vistrup authored 7 months ago
  
  4398f998
Nov 07, 2024
- add license · 7350e575
  Ralf Jung authored 7 months ago
  
  7350e575
- add LICENSE to islaris · a77b7b4e
  Michael Sammler authored 7 months ago
  
  a77b7b4e
Oct 31, 2024
- Merge branch 'master' of gitlab.inf.ethz.ch:ou-plf/iris-itree · 2617e52a
  Max Vistrup authored 7 months ago
  
  2617e52a
- Use `solve_ndisj` one more place. · fc7ff160
  Max Vistrup authored 7 months ago
  
  fc7ff160
Oct 28, 2024
- bump dependencies and fix build · ee2094b3
  Ralf Jung authored 7 months ago
  
  ee2094b3
Oct 26, 2024
- Add `spinlock` to `_CoqProject`. · 23f72661
  Max Vistrup authored 7 months ago
  
  23f72661
- Use `solve_ndisj` tactic instead of manual reasoning. · 19d461c6
  Max Vistrup authored 7 months ago
  
  19d461c6
Oct 25, 2024
- Formalize spinlock. · 7ac36d2f
  Max Vistrup authored 7 months ago
  
  7ac36d2f
- Merge branch 'master' of gitlab.inf.ethz.ch:ou-plf/iris-itree · 289141d8
  Max Vistrup authored 7 months ago
  
  289141d8
- Forgot to `git add`... · 570ab5a7
  Max Vistrup authored 7 months ago
  
  570ab5a7
- upstream things · 005abf79
  Michael Sammler authored 7 months ago
  
  005abf79
Oct 20, 2024
- Complete formalization of thread join. · ffea8026
  Max Vistrup authored 7 months ago
  
  ffea8026
Oct 18, 2024
- Merge branch 'master' of gitlab.inf.ethz.ch:ou-plf/iris-itree · bb82875d
  Max Vistrup authored 7 months ago
  
  bb82875d
- Extend proof-mode automation and begin porting `join` example to Iris (some... · b074df76
  Max Vistrup authored 7 months ago
  b074df76
Oct 16, 2024
- fix build · 7ed82692
  Michael Sammler authored 7 months ago
  
  7ed82692
- use fixpoint for compile_expr' · c0a9e823
  Michael Sammler authored 7 months ago
  
  c0a9e823
- Add a few examples for the interpreter. · 67aeca18
  Max Vistrup authored 7 months ago
  
  67aeca18
- fix remaining warnings · 7ee2ea4f
  Ralf Jung authored 7 months ago
  
  7ee2ea4f
- Merge branch 'master' of gitlab.inf.ethz.ch:ou-plf/iris-itree · cbbea091
  Ralf Jung authored 7 months ago
  
  cbbea091
- silence some warnings and fix the rest · 5bfc39f7
  Ralf Jung authored 7 months ago
  
  5bfc39f7
- Various minor improvements to make closer to paper. · 960026f1
  Max Vistrup authored 7 months ago
  
  960026f1
Oct 15, 2024
- Reword step adequacy theorem in terms of `step_irel` instead of `step_ifn`. · 81f371a2
  Max Vistrup authored 7 months ago
  
  81f371a2
- Prove `wp_atomic` for ExampleLang. · 246417a2
  Max Vistrup authored 7 months ago
  
  246417a2
- Match paper closer. · d817f417
  Max Vistrup authored 7 months ago
  
  d817f417
Oct 14, 2024
- Hide triggers behind abstractions. · a4303bb0
  Max Vistrup authored 7 months ago
  
  a4303bb0
- Merge branch 'master' of gitlab.inf.ethz.ch:ou-plf/iris-itree · bc2f1889
  Max Vistrup authored 7 months ago
  
  bc2f1889
- Add missing rule for ExampleLang program logic. · 67c7dc3c
  Max Vistrup authored 7 months ago
  
  67c7dc3c
- update axiom · db5e374b
  Michael Sammler authored 7 months ago
  
  db5e374b