Commits · d6f19e41b10720092ed607ed8db7940135a90d2d · Iris / Actris

Mar 25, 2020
- Ignore more stuff. · d6f19e41
  Robbert Krebbers authored 5 years ago
  
  d6f19e41
- Consistently use `Recv`. · 12dc9a35
  Robbert Krebbers authored 5 years ago
  
  12dc9a35
- Merge branch 'robbert/le_swap' into 'master' · 31806a14
  Robbert Krebbers authored 5 years ago
  
  Subprotocols with message swapping See merge request !2
  31806a14
- Remove some old `_proto`s in names. · 19f8a53a
  Robbert Krebbers authored 5 years ago
  
  19f8a53a
- Prove more intuitive derived subprotocol rules. · 085b698d
  Robbert Krebbers authored 5 years ago
  
  085b698d
- Fix some bad names. · 22cc3588
  Robbert Krebbers authored 5 years ago
  
  22cc3588
- Put ◇ modality in `iProto_le` so one can strip laters of timeless stuff. · 02ff4a94
  Robbert Krebbers authored 5 years ago
  
  02ff4a94
- Stronger swapping rule. · 6b7399d2
  Robbert Krebbers authored 5 years ago
  
  6b7399d2
- Make everything work; lots of refactoring. · cd70979b
  Robbert Krebbers authored 5 years ago
  
  cd70979b
- `skipN` function. · 72be456a
  Robbert Krebbers authored 5 years ago
  
  72be456a
- Experiment. · 4dc8fc9d
  Robbert Krebbers authored 5 years ago
  
  4dc8fc9d
- Tweaking. · 51ce4688
  Robbert Krebbers authored 5 years ago
  
  51ce4688
Mar 24, 2020
- WIP. · 7ca6ecc9
  Robbert Krebbers authored 5 years ago
  
  7ca6ecc9
- Close invariant under `iProto_le`. Remove updates from `iProto_le`. · a180e106
  Robbert Krebbers authored 5 years ago
  
  Symmetric proofs admitted.
  a180e106
- Params for `iProto_le`. · 0010b710
  Robbert Krebbers authored 5 years ago
  
  0010b710
- Break some very long lines. · c7701c44
  Robbert Krebbers authored 5 years ago
  
  c7701c44
- Fix some names. · 5c645163
  Robbert Krebbers authored 5 years ago
  
  5c645163
Mar 16, 2020
- Bump Iris (⊢ changes). · 8a13d685
  Robbert Krebbers authored 5 years ago
  
  8a13d685
Mar 13, 2020
- Update LICENSE. · 8b55e227
  Robbert Krebbers authored 5 years ago
  
  8b55e227
Mar 12, 2020
- update dependencies · 475a3a9f
  Ralf Jung authored 5 years ago
  
  475a3a9f
Feb 21, 2020
- update Makefile · f7ae375d
  Ralf Jung authored 5 years ago
  
  f7ae375d
Feb 17, 2020
- Remove more laters. · db4dff93
  Robbert Krebbers authored 5 years ago
  
  db4dff93
- Remove more useless laters. · 777d9fe1
  Robbert Krebbers authored 5 years ago
  
  777d9fe1
- Remove useless later. · 8957c470
  Robbert Krebbers authored 5 years ago
  
  8957c470
Nov 27, 2019
- Updated dependency commit hashes · 9a44a2d9
  Jonas Kastberg authored 5 years ago
  
  9a44a2d9
Nov 25, 2019
- Tweak comments a bit. · 16bf2d36
  Robbert Krebbers authored 5 years ago
  
  16bf2d36
- More README tweaking. · ee3c6ec1
  Robbert Krebbers authored 5 years ago
  
  ee3c6ec1
- Tweak README. · f803fca1
  Robbert Krebbers authored 5 years ago
  
  f803fca1
Nov 24, 2019
- Added more differences between paper and mechanisation to README · 2773194c
  Jonas Kastberg authored 5 years ago
  
  2773194c
Nov 22, 2019
- Added description of subtyping discrepancy in the README · a34d13a6
  Jonas Kastberg authored 5 years ago
  
  a34d13a6
Nov 21, 2019
- Bump Iris (make use of `excl_auth`). · 1bcc45db
  Robbert Krebbers authored 5 years ago
  
  1bcc45db
Nov 18, 2019
- Make example consistent with paper. · ba740097
  Robbert Krebbers authored 5 years ago
  
  ba740097
Nov 17, 2019
- update Makefile · 5e1d1f34
  Ralf Jung authored 5 years ago
  
  5e1d1f34
- Added another example for channel delegation · 7d4da4bd
  Jonas Kastberg authored 5 years ago
  
  7d4da4bd
Nov 16, 2019
- Another delegation example. · fb14f07d
  Robbert Krebbers authored 5 years ago
  
  fb14f07d
- Fix. · a0bc4d00
  Robbert Krebbers authored 5 years ago
  
  a0bc4d00
- Example with the loop. · 86f1cf3d
  Robbert Krebbers authored 5 years ago
  
  86f1cf3d
Nov 15, 2019
- Better names for basic examples. · 2efbf2f6
  Robbert Krebbers authored 5 years ago
  
  2efbf2f6
- More basic examples. · df678f5f
  Robbert Krebbers authored 5 years ago
  
  df678f5f
- Allow to use fancy updates in `iProto_le` · a7b129ac
  Robbert Krebbers authored 5 years ago
  
  a7b129ac