Commits · 1d1c47d6b40163775216146d68bf6005c4ee4aab · Amin Timany / iris-coq

Oct 30, 2015
- update gitignore · 1d1c47d6
  Ralf Jung authored 9 years ago
  
  1d1c47d6
- rename: filling function -> context function · d523141d
  Ralf Jung authored 9 years ago
  
  d523141d
- add a helpful comment · 5cca350d
  Ralf Jung authored 9 years ago
  
  5cca350d
- tune the filling axioms to make more sense · f4ecf1f2
  Ralf Jung authored 9 years ago
  
  f4ecf1f2
- also show htBind in ectx_lang · 99c799ee
  Ralf Jung authored 9 years ago
  
  99c799ee
- remove commented-out old axioms · 57f583d4
  Ralf Jung authored 9 years ago
  
  57f583d4
- refine filling axioms; add ectx_lang: a language defined in terms of... · d4992ced
  Ralf Jung authored 9 years ago
  
  refine filling axioms; add ectx_lang: a language defined in terms of evaluation contexts; show that it can do filling
  d4992ced
- show again the general bind rule · 6e850e1e
  Ralf Jung authored 9 years ago
  
  6e850e1e
- oO we can have a general bind rule... with very few assumptions about filling · bab069fd
  Ralf Jung authored 9 years ago
  
  bab069fd
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