Commits · 4229311f43e326535ea4e583020de66248fe9b60 · Iris / Actris

Feb 05, 2024
- First closed proof! · 4229311f
  Jonas Kastberg authored 1 year ago
  
  4229311f
- Added multi channels and more · e7a42450
  Jonas Kastberg authored 1 year ago
  
  e7a42450
- WIP multi_channel · cb563064
  Jonas Kastberg authored 1 year ago
  
  cb563064
- Proof of concept for synchronous resource transfer · 6a4c7570
  Jonas Kastberg authored 1 year ago
  
  6a4c7570
- Moved examples to other file. Added naive def of iProto_le · 4af1c72f
  Jonas Kastberg authored 1 year ago
  
  4af1c72f
- Solve remaining admits · 1fab9b4d
  Jonas Kastberg authored 1 year ago
  
  1fab9b4d
- Added proof of consistency for roundtrip example · 207ec3c0
  Jonas Kastberg authored 1 year ago
  
  207ec3c0
- Proved ghost theory stepping relation · 6d189579
  Jonas Kastberg authored 1 year ago
  
  6d189579
- Wrapped up API for multiparty ghost theory · 4d5fbe48
  Jonas Kastberg authored 1 year ago
  
  4d5fbe48
- WIP: Proof of iProto_consistent_step · 0baa9a22
  Jonas Kastberg authored 1 year ago
  
  0baa9a22
- WIP: Multiparty definition · eda6b395
  Jonas Kastberg authored 1 year ago
  
  eda6b395
- Synchronous ghost theory for binary session types · c3a22c76
  Jonas Kastberg authored 1 year ago
  
  c3a22c76
- Bump Coq 8.19 · 00ecc263
  Jonas Kastberg authored 1 year ago
  
  00ecc263
Feb 02, 2024
- Merge branch 'ci/coq' into 'master' · f54aa1f1
  Ralf Jung authored 1 year ago
  
  bump to Coq 8.18 See merge request !33
  f54aa1f1
- bump to Coq 8.18 · 1b43afae
  Ralf Jung authored 1 year ago
  
  1b43afae
- update dependencies · c43e0aef
  Ralf Jung authored 1 year ago
  
  c43e0aef
Jan 31, 2024
- Improved fork_chan proofmode · dfef4e62
  Jonas Kastberg authored 1 year ago
  
  dfef4e62
Jan 30, 2024
- Aligned fork_chan tactic binders with protocols · d36fe30f
  Jonas Kastberg authored 1 year ago
  
  d36fe30f
- Renamed start_chan to fork_chan to conform with LinearActris · ac878307
  Jonas Kastberg authored 1 year ago
  
  ac878307
Jan 28, 2024
- Opened proto scope to avoid superfluous delimiters · ece0a511
  Jonas Kastberg authored 1 year ago
  
  ece0a511
- Basic tactic support for resolving new_chan · 48de4691
  Jonas Kastberg authored 1 year ago
  
  48de4691
Nov 20, 2023
- Bumped opam file to new Iris version · b03078c9
  Jonas Kastberg authored 1 year ago
  
  b03078c9
- Bumped Iris · 4f724411
  Jonas Kastberg authored 1 year ago
  
  4f724411
Nov 06, 2023
- update readme · 227e5403
  Ralf Jung authored 1 year ago
  
  227e5403
- update dependencies · 78ee0888
  Ralf Jung authored 1 year ago
  
  78ee0888
Oct 05, 2023
- update dependencies · e8f2f193
  Ralf Jung authored 1 year ago
  
  e8f2f193
- Revert "stick to 8.17 for nightly testing for now" · 04183d44
  Ralf Jung authored 1 year ago
  
  This reverts commit 4243284b. Robbert's previous commit should make this 8.18-compatible.
  04183d44
Oct 04, 2023
- Tweak proof so it does not run into https://github.com/coq/coq/issues/18126 on Coq 8.18. · 9cbf4cdd
  Robbert Krebbers authored 1 year ago
  
  The new proof avoids `setoid_rewrite` and is just as good, so no need to revert once Coq is fixed.
  9cbf4cdd
- stack on 8.17 for nightly testing for now · 4243284b
  Ralf Jung authored 1 year ago
  
  4243284b
Oct 03, 2023
- update dependencies · 9301d9e0
  Ralf Jung authored 1 year ago
  
  9301d9e0
Aug 31, 2023
- update dependencies · 25d7353e
  Ralf Jung authored 1 year ago
  
  25d7353e
Aug 04, 2023
- Bump Iris (iIntros starts proof). · 8e787f74
  Robbert Krebbers authored 1 year ago
  
  8e787f74
May 04, 2023
- update dependencies · 477d92e9
  Ralf Jung authored 1 year ago
  
  477d92e9
May 02, 2023
- Bump Iris; bump minimal Coq version to 8.17. · e5b60710
  Robbert Krebbers authored 1 year ago
  
  e5b60710
- centrally control the Coq version to test every night · db1431da
  Ralf Jung authored 1 year ago
  
  db1431da
Apr 18, 2023
- Do not rely on conversion of maps. · e76e6e8d
  Robbert Krebbers authored 1 year ago
  
  e76e6e8d
Mar 09, 2023
- More uses of `iCombine .. gives`. · bd4b6aa2
  Robbert Krebbers authored 2 years ago
  
  bd4b6aa2
- Bump Iris (beautify code for `iCombine .. gives`). · ee751d70
  Robbert Krebbers authored 2 years ago
  
  ee751d70
Mar 07, 2023
- Oops, forgot `as`... · fe99c059
  Robbert Krebbers authored 2 years ago
  
  fe99c059
- dist_later_intro fixes. · 75b7a0b4
  Robbert Krebbers authored 2 years ago
  
  75b7a0b4