Skip to content
Snippets Groups Projects
Select Git revision
  • clairvoyant
  • erasure
  • erasure-squashed
  • erasure_backup
  • janno/early-scopes
  • janno/hoare-notation
  • jh_coreless_cmras
  • jh_inductive_pairs
  • jh_partial_core
  • lang_lemmas
  • less_canonical
  • master default
  • monotone
  • mra-changelog
  • primitive_sealing
  • ralf/magic-singleton
  • rename
  • iris-2.0
  • iris-2.0-rc2
  • iris-2.0-rc1
  • iris-1.1
  • iris-1.0
  • hope-2015-coq-1
  • appendix-1.0.0
  • appendix-1
25 results
You can move around the graph by using the arrow keys.
Created with Raphaël 2.2.011Feb10985432131Jan302927262523222120191817161413129865422Dec21161514118423Nov22201918171612119630Oct2928272316151431Aug16Jul24Jun2215115432131May302928272625161514131211723Apr141311109872131Mar302928272524232019rename uPred_own -> uPred_ownMadd a tactic to solve non-expansiveness goalshard-wire the auth construction to timeless CMRAsauth commentsrename own lemmas in upred to ownM, to avoid overlapping namesMerge branch 'master' of gitlab.mpi-sws.org:FP/iris-coqprove auth_pvs!slightly simplify some proofs in upred.vRemove some left-over junk.CMRAs with identity element are inhabited.No longer use option for local updates.Merge branch 'master' of gitlab.mpi-sws.org:FP/iris-coqHack to avoid substitution perform Coq-level delta reduction.Merge branch 'master' of gitlab.mpi-sws.org:FP/iris-coqintroduce a notion oflocal updates (up for discussion) and use it to formulate the auth rulesNotation for literals.Fix level for let notation.Remove let as a built-in and make it syntactic sugar again.make auth_closing less stupidmake auth.v work againMerge branch 'master' of gitlab.mpi-sws.org:FP/iris-coqprove auth_closing :)Merge branch 'master' of gitlab.mpi-sws.org:FP/iris-coqCOFE distance is no longer trivial at index 0.complete auth_opened :)start work on the auth constructionseparate gid and gnamechange notation for view shifts to ={E}=>change notation of step-indexed equality to ≡{n}≡remove some unused typeclasses and notation: EquivE and SubsetEqEmake some nested function calls in heap_lang/ more readableignore some tmp emacs filesno reason for this primeRemove Unshelve hack in ghost_ownership.Fix some identation.Typeclass Opacity and Params for inv.Seperate derived rules for own and valid in upred.Make let a built-in connective of heap_lang.Change the level of wand so it is more like the implication.Change the level of view shifts so it is more like the implication.