Commits · bd440d3dd917f1571ba24c0c3d88d1c48b3ebd3d · Iris / lambda-rust

May 10, 2021
- Merge remote-tracking branch 'origin/master' into masters/weak_mem · bd440d3d
  Jacques-Henri Jourdan authored 3 years ago
  
  bd440d3d
May 07, 2021
- Update dependency · c4bbed6c
  Hai Dang authored 3 years ago
  
  c4bbed6c
- Merge branch 'jh/fn_notation' into 'master' · 58bfc65c
  Ralf Jung authored 3 years ago
  
  Improve notations for functions See merge request !23
  58bfc65c
May 05, 2021
- Update dependencies · f32cecf4
  Hai Dang authored 3 years ago
  
  f32cecf4
- update dependencies · ec9fdf59
  Ralf Jung authored 3 years ago
  
  ec9fdf59
- update dependencies · ec6af5ad
  Ralf Jung authored 3 years ago
  
  ec6af5ad
May 04, 2021
- The introduction pattern \!# is deprecated. Replace by \!>. · 9c1d9abd
  Jacques-Henri Jourdan authored 3 years ago
  
  9c1d9abd
- Improve notations for functions · b234965c
  Jacques-Henri Jourdan authored 3 years ago
  
  We use fnrec: for recursive functions and fn: for non-recursve functions. This is both shorter and closer to Rust.
  b234965c
May 01, 2021
- Nit. · 75f6aaae
  Jacques-Henri Jourdan authored 3 years ago
  
  75f6aaae
Apr 28, 2021
- fix CI config · 0557ef4c
  Ralf Jung authored 3 years ago
  
  0557ef4c
- don't test against Coq master (it is broken) · bd727416
  Ralf Jung authored 3 years ago
  
  bd727416
- don't test against Coq master (it is broken) · b6389b47
  Ralf Jung authored 3 years ago
  
  b6389b47
Apr 20, 2021
- Bump std++ (multisets). · 302e8e89
  Robbert Krebbers authored 4 years ago
  
  302e8e89
- Bump std++ (multisets). · 4e3fabc0
  Robbert Krebbers authored 4 years ago
  
  4e3fabc0
Apr 14, 2021
- Bump gpfsl · 58864e5b
  Hai Dang authored 4 years ago
  
  58864e5b
Mar 16, 2021
- Merge branch 'msammler/update-iris' into 'master' · 9f72ef66
  Ralf Jung authored 4 years ago
  
  Update iris dependency See merge request !22
  9f72ef66
- Update iris dependency · c961dd7b
  Michael Sammler authored 4 years ago
  
  c961dd7b
Mar 15, 2021
- fix warnings · 8c43dc46
  Ralf Jung authored 4 years ago
  
  using Tej's script from iris!594 (comment 60292)
  8c43dc46
- bump the Coq version we test · 3cd6ebad
  Ralf Jung authored 4 years ago
  
  3cd6ebad
- Merge branch 'ci/ralf/ghostcell' into 'master' · 85369545
  Ralf Jung authored 4 years ago
  
  add GhostCell proof See merge request !19
  85369545
Mar 11, 2021
- more comments explaining the weakened typing rule · 0e60fa20
  Ralf Jung authored 4 years ago
  
  0e60fa20
- add GhostCell proof by Joshua Yanovski · 97946ce6
  Ralf Jung authored 4 years ago
  
  97946ce6
- add BrandedVec proof by Joshua Yanovski · 4376ac7f
  Ralf Jung authored 4 years ago
  
  4376ac7f
- make external lifetime context inclusion syntactic, and adjust type system and existing proofs · ac7ba2d6
  Ralf Jung authored 4 years ago
  
  ac7ba2d6
- add derived 'meta' mechanism to lifetime logic: associate a lifetime with metadata (via a gname) · 1da46577
  Ralf Jung authored 4 years ago
  
  1da46577
- add 'syntactic' notion of lifetim inclusion and prove basic lemmas about it · 572c354a
  Ralf Jung authored 4 years ago
  
  572c354a
- prove that Skip is atomic · 719c409c
  Ralf Jung authored 4 years ago
  
  719c409c
Mar 09, 2021
- update dependencies · 7a5a1733
  Ralf Jung authored 4 years ago
  
  7a5a1733
Mar 07, 2021
- Bump. · d61f7e25
  Jacques-Henri Jourdan authored 4 years ago
  
  d61f7e25
- Bump · a96ed1bf
  Jacques-Henri Jourdan authored 4 years ago
  
  a96ed1bf
Mar 06, 2021
- update dependencies · 1d86c738
  Ralf Jung authored 4 years ago
  
  1d86c738
Mar 03, 2021
- update dependencies · ab1110a9
  Ralf Jung authored 4 years ago
  
  ab1110a9
Feb 16, 2021
- update dependencies · a38a1915
  Ralf Jung authored 4 years ago
  
  a38a1915
- update dependencies · c6235271
  Ralf Jung authored 4 years ago
  
  c6235271
Feb 14, 2021
- Bump Iris. · 707db861
  Robbert Krebbers authored 4 years ago
  
  707db861
- Bump Iris. · b4038b7b
  Robbert Krebbers authored 4 years ago
  
  b4038b7b
Feb 12, 2021
- add variant of diverging_static for arbitrary invariant lifetime positions · d1a2a68f
  Ralf Jung authored 4 years ago
  
  d1a2a68f
- diverging_static can now be checked in the type system · 5b40fd70
  Ralf Jung authored 4 years ago
  
  5b40fd70
Feb 11, 2021
- show variant of equalization with the static lifetime · 57f71459
  Ralf Jung authored 4 years ago
  
  57f71459
- update dependencies · dcc0d0db
  Ralf Jung authored 4 years ago
  
  dcc0d0db