Commits · 42f3528f4bfdad3ce17c7731a4a0b524ba9a98dc · Iris / lambda-rust

Feb 18, 2017

Jacques-Henri Jourdan authored 8 years ago

* Also, removed the box from the definition of typing judgments, so that we can frame resources around them.

42f3528f

Feb 17, 2017

Make (most of) the typing lemmas implications in Iris. · 41044564

Jacques-Henri Jourdan authored 8 years ago

This requires using iApply instead of eapply to use them.

TODO : have an Iris version of Forall2, so that the lemmas for typing switches can be implications in Iris.

41044564

Feb 16, 2017
- Oops, forgot to bump Iris. · c0757d53
  Robbert Krebbers authored 8 years ago
  
  c0757d53
- Use Iris' iso_ofe infrastructure for types and seal off equiv and dist. · ce54063e
  Robbert Krebbers authored 8 years ago
  
  ce54063e
Feb 15, 2017
- Bump Iris version and make use of improved solve_ndisj. · 98be0049
  Robbert Krebbers authored 8 years ago
  
  98be0049
- Bump Iris and fix stuff. · 3e2ae1fc
  Robbert Krebbers authored 8 years ago
  
  3e2ae1fc
- Port Iris 84d78426: Remove an Ltac hack that was there for unknown reason. · 41dd8385
  Robbert Krebbers authored 8 years ago
  
  41dd8385
- Merge branch 'master' of https://gitlab.mpi-sws.org/FP/LambdaRust-coq · 855e5e45
  Ralf Jung authored 8 years ago
  
  855e5e45
- avoid using wp_bind; use wp_apply instead · c10260ac
  Ralf Jung authored 8 years ago
  
  c10260ac
- Remove uses of iStartProof, which is intended as being an internal tactic. · ec40350b
  Jacques-Henri Jourdan authored 8 years ago
  
  ec40350b
Feb 13, 2017
- Bump iris. Simplify some proofs. · 6d36b8cf
  Jacques-Henri Jourdan authored 8 years ago
  
  6d36b8cf
- refcell: split switching back to the type system and chekcing the first instruction into two steps · f4e566ec
  Ralf Jung authored 8 years ago
  
  f4e566ec
- update Cell to prove replace instead of just set (like in latest nightly Rust) · 0b73ab70
  Ralf Jung authored 8 years ago
  
  0b73ab70
Feb 12, 2017
- Bump Iris and remove a FIXME. · 9aeb8f2b
  Robbert Krebbers authored 8 years ago
  
  9aeb8f2b
- Remove another FIXME. · 3c5e3622
  Robbert Krebbers authored 8 years ago
  
  3c5e3622
Feb 11, 2017
- Bump Iris and fix several TODOs and FIXMEs. · f1f3836d
  Robbert Krebbers authored 8 years ago
  
  f1f3836d
- update lang to use heap_lang style: merge lifting.v and derived.v · 53a237b5
  Ralf Jung authored 8 years ago
  
  53a237b5
- show join_handle_subtype inside the logic · 8ba197a1
  Ralf Jung authored 8 years ago
  
  8ba197a1
- allow subtyping for join_handle · cf7f3ffc
  Ralf Jung authored 8 years ago
  
  cf7f3ffc
- note a TODO · 3c6d0d23
  Ralf Jung authored 8 years ago
  
  3c6d0d23
- type the join function · 3bf41e48
  Ralf Jung authored 8 years ago
  
  3bf41e48
Feb 10, 2017
- prove that spawn can return a join handle · 3b7a99c2
  Ralf Jung authored 8 years ago
  
  3b7a99c2
- wp_alloc provides a vector of allocated values · 4622cb39
  Ralf Jung authored 8 years ago
  
  4622cb39
- leave a TODO · 9edc1b15
  Ralf Jung authored 8 years ago
  
  9edc1b15
- Merge branch 'master' of https://gitlab.mpi-sws.org/FP/LambdaRust-coq · 9b8d36ce
  Ralf Jung authored 8 years ago
  
  9b8d36ce
- adapt the locking approach for value-lambdas like we did in iris.heap_lang · 6dcf60e2
  Ralf Jung authored 8 years ago
  
  6dcf60e2
Feb 09, 2017
- Bumb Iris version. · a4e9ac66
  Robbert Krebbers authored 8 years ago
  
  a4e9ac66
- Remove obsolete TODO. · 87413b96
  Robbert Krebbers authored 8 years ago
  
  87413b96
- prove a spawn-join primitive · 7532af1b
  Ralf Jung authored 8 years ago
  
  The interface is slightly more flexible than the one on iris.heap_lang to support continuation passing style
  7532af1b
- update build system · b7247b08
  Ralf Jung authored 8 years ago
  
  b7247b08
- Merge branch 'master' of gitlab.mpi-sws.org:FP/LambdaRust-coq · 3dd95b21
  Jacques-Henri Jourdan authored 8 years ago
  
  3dd95b21
- Iris master. · 36b7acc9
  Jacques-Henri Jourdan authored 8 years ago
  
  36b7acc9
- Merge branch 'master' of https://gitlab.mpi-sws.org/FP/LambdaRust-coq · 108063ea
  Ralf Jung authored 8 years ago
  
  108063ea
- prove thread::spawn · 1d5970bd
  Ralf Jung authored 8 years ago
  
  1d5970bd
- improve function type notation · f6a263a8
  Ralf Jung authored 8 years ago
  
  f6a263a8
- Merge branch 'master' of gitlab.mpi-sws.org:FP/LambdaRust-coq · 5682cfe0
  Jacques-Henri Jourdan authored 8 years ago
  
  5682cfe0
- update iris to use stdpp · 10b7a540
  Ralf Jung authored 8 years ago
  
  10b7a540
- update buildsystem · 7594024f
  Ralf Jung authored 8 years ago
  
  7594024f
Feb 08, 2017
- use new function type notation for examples · d5ab6f51
  Ralf Jung authored 8 years ago
  
  d5ab6f51
- notation for the function type · 052d9f00
  Ralf Jung authored 8 years ago
  
  052d9f00