Commits · 354cf991b561ba97035ec74781433df7949ccefe · Iris / ReLoC

Jun 11, 2020
- More type notations. · 354cf991
  Robbert Krebbers authored 4 years ago
  
  354cf991
Jun 03, 2020
- Working on the helping_wrapper.v · 89580783
  Dan Frumin authored 4 years ago
  
  89580783
- minor fixes in the lock spec and in the CG stack · 6830674c
  Dan Frumin authored 4 years ago
  
  6830674c
May 31, 2020
- simplify the bit refinement · 83042e9a
  Dan Frumin authored 4 years ago
  
  83042e9a
May 28, 2020
- Bump Iris (Z_scope). · 6fc57892
  Robbert Krebbers authored 4 years ago
  
  6fc57892
May 27, 2020
- update dependencies, fix for lifting rename · 03fc4762
  Ralf Jung authored 4 years ago
  
  03fc4762
May 26, 2020
- Bump Iris (free operation). · 44ca81fd
  Robbert Krebbers authored 4 years ago
  
  44ca81fd
May 25, 2020
- bit of cleanup · a8a8439a
  Dan Frumin authored 4 years ago
  
  a8a8439a
- simplify `tac_rel_load_r` · 9e0d651a
  Dan Frumin authored 4 years ago
  
  9e0d651a
May 24, 2020
- Bump Iris (sbi removal). · b56c7cc7
  Robbert Krebbers authored 4 years ago
  
  b56c7cc7
May 18, 2020
- update gitignore · 25eb1239
  Ralf Jung authored 4 years ago
  
  25eb1239
- update Iris · 15526ec5
  Ralf Jung authored 4 years ago
  
  15526ec5
May 13, 2020
- Use is_stack predicate for the right hand side · aeaaf8b2
  Dan Frumin authored 4 years ago
  
  aeaaf8b2
May 06, 2020
- Ticket lock refinement using HOCAP-style specs · 0e7e1e07
  Dan Frumin authored 4 years ago
  
  0e7e1e07
May 04, 2020
- a tiny clean up · 3c05b1ae
  Dan Frumin authored 4 years ago
  
  3c05b1ae
Apr 29, 2020
- better handling of rel_pure_l/r · 5c942d31
  Dan Frumin authored 4 years ago
  
  5c942d31
- Fix a warning · ac3a3e4d
  Dan Frumin authored 4 years ago
  
  ac3a3e4d
- More work on tp_ tactics · 5d15373a
  Dan Frumin authored 4 years ago
  
  - All tp_ tactics work without explicit modalities in the goal; - All tp_ tactics simplify the ghost thread pool points-to; - Proof term size improvements
  5d15373a
Apr 28, 2020
- fix the tp_ tactics · c32e111d
  Dan Frumin authored 4 years ago
  
  c32e111d
Apr 23, 2020
- Simplify `revoke_offer_l` further · 15dac0c4
  Dan Frumin authored 4 years ago
  
  15dac0c4
Apr 22, 2020
- Cleanup in the stack with helping proof · 26051162
  Dan Frumin authored 4 years ago
  
  26051162
- Make the helping stack proof abstract in the offers specs (almost?) · 753db937
  Dan Frumin authored 4 years ago
  
  753db937
- Simplify the stack with helping refinement. · 6fee530c
  Dan Frumin authored 4 years ago
  
  6fee530c
Apr 21, 2020
- Merge branch 'master' of gitlab.mpi-sws.org:iris/reloc · 64791382
  Dan Frumin authored 4 years ago
  
  64791382
- wk_incr · 15185169
  Dan Frumin authored 4 years ago
  
  15185169
Apr 18, 2020
- update dependencies · a96c4a03
  Ralf Jung authored 4 years ago
  
  a96c4a03
Apr 13, 2020
- Merge branch 'master' of gitlab.mpi-sws.org:iris/reloc · 926738e3
  Dan Frumin authored 4 years ago
  
  926738e3
- a bit of cleanup in bit.v · 900b58ae
  Dan Frumin authored 4 years ago
  
  900b58ae
Apr 09, 2020
- quickfix for _CoqProject · ae8a85e5
  Dan Frumin authored 4 years ago
  
  ae8a85e5
- Bump Iris. · 9487c4c3
  Robbert Krebbers authored 4 years ago
  
  9487c4c3
Apr 05, 2020
- Refinement proof with HOCAP specs. · bb4669b4
  Dan Frumin authored 4 years ago
  
  bb4669b4
- HOCAP specs for the counter · 48090e44
  Dan Frumin authored 4 years ago
  
  48090e44
- Merge commit 'f4619355 ' · ecd44ff2
  Dan Frumin authored 4 years ago
  
  ecd44ff2
- Add typing for values. · 8786f3ef
  Dan Frumin authored 5 years ago
  
  8786f3ef
- Ignore more. · e46427d5
  Robbert Krebbers authored 4 years ago
  
  e46427d5
- Bump Iris. · 42e0d03d
  Robbert Krebbers authored 4 years ago
  
  42e0d03d
Apr 03, 2020
- update dependencies · 232c2cac
  Ralf Jung authored 4 years ago
  
  232c2cac
Mar 16, 2020
- Bump Iris (⊢ changes). · fdb975a5
  Robbert Krebbers authored 5 years ago
  
  fdb975a5
Mar 13, 2020
- Update LICENSE. · 03c65e92
  Robbert Krebbers authored 5 years ago
  
  03c65e92
Mar 06, 2020
- Ordering induced by ⊕ conincides with contextual refinement · f4619355
  Dan Frumin authored 5 years ago
  
  f4619355