Commits · 4d68e9b957845e514914c208f7f2629ec97b3ddb · Amin Timany / iris-coq

Oct 29, 2015
- *oops* I renamed that one... · 4d68e9b9
  Ralf Jung authored 9 years ago
  
  4d68e9b9
- update the 'stupid' language in iris_check · 15c81ecd
  Ralf Jung authored 9 years ago
  
  15c81ecd
- *oops* make things compile again · 27b5ff7c
  Ralf Jung authored 9 years ago
  
  27b5ff7c
- done re-establishing lifting · 837582ac
  Ralf Jung authored 9 years ago
  
  837582ac
- complete stateful lifting · d4143186
  Ralf Jung authored 9 years ago
  
  d4143186
Oct 28, 2015
- re-establish the stateful lifting · 56fd0a20
  Ralf Jung authored 9 years ago
  
  56fd0a20
Oct 27, 2015
- reestablish derived HT properties · 337c3a2a
  Ralf Jung authored 9 years ago
  
  337c3a2a
- reestablish basic HT properties · 0f438963
  Ralf Jung authored 9 years ago
  
  0f438963
- remove commented-out axioms; fix weakest-pre and also change it to no longer... · 5f52726a
  Ralf Jung authored 9 years ago
  
  remove commented-out axioms; fix weakest-pre and also change it to no longer contain the final view shift; re-establish adequacy
  5f52726a
Oct 23, 2015
- fork be gone. iris_meta broken · f7c9909f
  Janno authored 9 years ago
  
  f7c9909f
Oct 16, 2015
- Show the relationship between safe expressions and thread pool reduction · 95c7a3f3
  Ralf Jung authored 9 years ago
  
  95c7a3f3
Oct 15, 2015
- improve benchmark script · 0b364bb5
  Ralf Jung authored 9 years ago
  
  0b364bb5
Oct 14, 2015
- show that fork is atomic! · 7abb5b47
  Ralf Jung authored 9 years ago
  
  7abb5b47
- weakest pre: forked thread can have full mask. as a result, the fork rule got stronger. · a3260824
  Ralf Jung authored 9 years ago
  
  a3260824
Aug 31, 2015
- agreement: simplify metric · bd5a870b
  Ralf Jung authored 9 years ago
  
  bd5a870b
Jul 16, 2015
- Merge branch 'master' of git.fp.mpi-sws.org:nowbook · 2ae72771
  Janno authored 9 years ago
  
  2ae72771
- inv is contractive · e0391117
  Janno authored 9 years ago
  
  e0391117
Jun 24, 2015
- show that for AFrame, it is good enough to have any non-value · 9eb6d400
  Ralf Jung authored 9 years ago
  
  9eb6d400
- prove the close relationship between wp on values and non-mask-changing view shifts · b107b14e
  Ralf Jung authored 9 years ago
  
  b107b14e
Jun 22, 2015
- show some things about the magic wand · 6aa6a91f
  Ralf Jung authored 9 years ago
  
  6aa6a91f
Jun 15, 2015
- use 'return _' to tell Program to behave · fd8e3149
  Ralf Jung authored 9 years ago
  
  fd8e3149
- slight simpl tuning · cb0a20de
  Ralf Jung authored 9 years ago
  
  cb0a20de
Jun 11, 2015
- coq-ho: update README, remove commented-out robust safety (in preparation for HOPE) · 0ce42920
  Ralf Jung authored 9 years ago
  
  hope-2015-coq-1
  
  0ce42920
Jun 05, 2015
- notation for fdStrongUpdate · f8ca50fa
  Janno authored 9 years ago
  
  f8ca50fa
- show that owning a ghost-unit can be boxed · e11f52aa
  Ralf Jung authored 9 years ago
  
  e11f52aa
Jun 04, 2015
- Predom is good enough for RAConstr · 1f918268
  Ralf Jung authored 9 years ago
  
  1f918268
- some minor changes for better 8.5-compatibility · 9a797c9f
  Ralf Jung authored 9 years ago
  
  9a797c9f
- prepare MetricCore better for Coq 8.5 · 024e8089
  Ralf Jung authored 9 years ago
  
  024e8089
- some small simplifications to agreement · 3ba58191
  Ralf Jung authored 9 years ago
  
  3ba58191
Jun 03, 2015
- proved timeless_impl · 24b3e476
  Janno authored 9 years ago
  
  24b3e476
- *oops* fix fallout from box conversion · f6ef6427
  Ralf Jung authored 9 years ago
  
  f6ef6427
- prove the last missing view shift rules · 160cc780
  Ralf Jung authored 9 years ago
  
  160cc780
- add sugar for defining SPreds, this also makes them print nicer in some cases · cae9dd85
  Ralf Jung authored 9 years ago
  
  cae9dd85
Jun 02, 2015
- work on timelessness · f6d457c4
  Ralf Jung authored 9 years ago
  
  f6d457c4
- show the missing axioms for later and box · 8a4beb3e
  Ralf Jung authored 9 years ago
  
  8a4beb3e
- simplify wsat a bit · 96588154
  Ralf Jung authored 9 years ago
  
  96588154
Jun 01, 2015
- come more small comments · a4b217f3
  Ralf Jung authored 9 years ago
  
  a4b217f3
- document some things · 2e7b1a21
  Ralf Jung authored 9 years ago
  
  2e7b1a21
May 31, 2015
- construct a CMRAExt for Agreement. This completes the CMRAExt for the final... · 47fc5102
  Ralf Jung authored 9 years ago
  
  construct a CMRAExt for Agreement. This completes the CMRAExt for the final world, which completes the entire construction - it's all admit-free! :-))
  47fc5102
- show that finite partial functions preserve "CMRAExt" · 41e78456
  Ralf Jung authored 9 years ago
  
  41e78456