Skip to content
Snippets Groups Projects
Select Git revision
  • atomic
  • ci/3.1.0
  • ci/debug
  • ci/janno/debug-opam
  • ci/janno/vmcast
  • ci/ralf/ci
  • ci/ralf/pm_red
  • ci/robbert/into_val_pures
  • ci/stability
  • ci/value_constructor
  • fast_string
  • iris-3.0
  • iris-3.1
  • janno/metacoq
  • jh/done_contradiction
  • jh/evar_iframe
  • jh/independent_metric
  • jh/sprop_upred
  • jh_inductive_pairs
  • joe/bupd_derived
  • 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
30 results
You can move around the graph by using the arrow keys.
Created with Raphaël 2.2.018Oct17161514131210976543228Sep272120191514131298765432131Aug302928272625242322212019181716141110986542128Jul272625232221201918161513121165432130Jun28272625242321201918171615148761docs: use new notation of None and invalid CMRA elementslet's try not to make those macro names too longupdate iris.stybe even more verbose about licensingMerge branch 'ralf/docs-license' into 'master' Be explicit about the CMRA on optionadd a LICENSE file summarizing our licensingput the appendix under CC-BY 4.0fix CHANGELOG markupFix state CMRA.Use \nat macro.Define \List macro and use the more commonly used \vec for denoting lists.Make better use of \Val, \State, \Expr macros.Move language section to its own file.Define macro for singleton map and use it.Remove obsolete file encodings.tex.Merge branch 'master' of gitlab.mpi-sws.org:FP/iris-coqLifting lemmas do no longer have in hypothsesis that the expression is not a value.docs: fix auth introdocs: rename some section labelsdocs: describe authoritativeCHANGELOG: program_logic/auth is backOnly one direction of assoc and comm for separating conjunction is needed.Merge branch 'master' of gitlab.mpi-sws.org:FP/iris-coqRename some rules : pvs -> vup.docs: hyperlink some rulesWe already have \maybe for the option typeMerge branch 'master' of gitlab.mpi-sws.org:FP/iris-coqdocs: fix some newlinesMerge iris.sty with Iris 3.0 paper.Merge branch 'master' of gitlab.mpi-sws.org:FP/iris-coqdocs: rule nitpickingMerge branch 'master' of gitlab.mpi-sws.org:FP/iris-coqThe mask of the VS for allocating invariant has an empty mask.Merge branch 'master' of gitlab.mpi-sws.org:FP/iris-coqMake everything compile with Coq 8.6get rid of the strange pvs_intro'; use pvs_intro_mask insteadexplain the use of \bot for masksCorrect the Inv-alloc rule.rename program_logic.{ownership -> wsat}. It really is about world satisfaction and invariants more than about ownership.