Skip to content
Snippets Groups Projects
Select Git revision
  • ci/debug
  • ci/for_proph
  • ci/general-contractive
  • ci/hai/siProp
  • ci/janno/strict-tc-resolution
  • ci/msammler/nb_state
  • ci/ralf/Z_of_nat
  • ci/ralf/bi-language
  • ci/robbert/big_op_binder
  • ci/robbert/contractive_ne
  • ci/robbert/coq_bug_7773
  • ci/robbert/faster_iDestruct
  • ci/robbert/faster_iDestruct2
  • ci/robbert/faster_iFresh_joe
  • ci/robbert/frame_fractional
  • ci/robbert/iFrame
  • ci/robbert/into_fupd
  • ci/robbert/into_val_pures
  • ci/robbert/kill_locked_value_lambdas
  • ci/robbert/mapsto_persist
  • iris-4.0.0
  • iris-3.6.0
  • iris-3.5.0
  • iris-3.4.0
  • iris-3.3.0
  • iris-3.2.0
  • iris-3.1.0
  • iris-3.0.0
  • 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
36 results
You can move around the graph by using the arrow keys.
Created with Raphaël 2.2.023Jul2221201918161297528Jun262524232221201918171514131211109876543231May282726252120191817131211975230Apr2922201918151413121186527Mar2524232218171514131210986543124Feb23221917161514131211105432129Jan282726252320191715141312875424Dec231918161110976432130Nov2726231918131211Merge branch 'robbert/curry' into 'master'fix iris-bot scriptupdate dependenciesMerge branch 'robbert/fixpoint' into 'master'Apply 1 suggestion(s) to 1 file(s)Merge branch 'robbert/big_andL_orL' into 'master'CHANGELOG.Add non-expansive instances for `curry` and friends.Add some missing lemmas for `big_andL` and `big_orL`.CHANGELOG.Bump std++.Strengthen `bi_mono_pred` to ensure that functions are non-expansive.update dependenciesMerge branch 'ralf/atomic-wp-mask' into 'master'Bump std++ (curry/uncurry)update dependencieschangelogavoid line-breaking within the mask part of AU/AACCmake atomic_wp mask work more like wp maskupdate dependenciesMerge branch 'ralf/fixpoint' into 'master'Merge branch 'persistent-fractional' into 'master'consistent changelog formattingpersistent_fractional: strengthen like bi.persistent_sep_dupalso use □ in bi_{least,greates}_fixpointMerge branch 'robbert/bi_mono_pred' into 'master'CHANGELOG.State `bi_mono_pred` using `□`/`-∗` instead of `<pers>`/`→`.update dependenciesInitial experiment with internal_eq for bi with siProp embeddingci/hai/siPropci/hai/siPropAdd internal algebra properties for siProp, and derive some of those for bi with siProp embeddingGeneralize cmra_valid for any bi with siProp embeddingAdd more embedding instances for siPropAdd embedding of siProp into uPredMinimize primitive rules for embed and emp_valid; Partially fix notations; Fix some commentsMake an unseal LocalFinish redefining several uPred's connectives as siPropInitial work on implementing various uPred connectives in siPropprove 'weird' monotonicity rule for logatom triple masksadd comment in iris.sty
Loading