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.022Jul21201918161297528Jun262524232221201918171514131211109876543231May282726252120191817131211975230Apr2922201918151413121186527Mar2524232218171514131210986543124Feb23221917161514131211105432129Jan282726252320191715141312875424Dec231918161110976432130Nov2726231918131211CHANGELOG.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.styMerge branch 'ralf/big_sepS_delete_2' into 'master'more implicitstrengthen lemmasadd big_sepS_insert_2add big_sepS_delete_2update dependenciesMerge branch 'ralf/int-div' into 'master'mention a concrete languageupdate dependencies
Loading