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.013Oct1210976543228Sep272120191514131298765432131Aug302928272625242322212019181716141110986542128Jul272625232221201918161513121165432130Jun2827262524232120191817161514876131MayMerge 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.auth tweaks.shorten heap_lang/adequacy prooffix heap_lang/adequacyMerge branch 'master' of gitlab.mpi-sws.org:FP/iris-coqthe resurrection of program_logic/authMake validity of STS fragments require a witness.Merge branch 'master' of gitlab.mpi-sws.org:FP/iris-coqupdate CHANGELOGdocs: finish up accessors for now; let's just see what we write for the paperAdd PersistentP instances for own(S).docs: make Robbert happy, don't use 2 as mnemonic for "to"docs: Be precise about embedding meta-level assertions for the adequacy statementMerge branch 'robbert/local_updates'docs: Units no longer have to be discrete.docs: some talk about accessorsMerge branch 'master' of gitlab.mpi-sws.org:FP/iris-coqdocs: invariant namespacesAdd rewrite lemma for frac_opuse a nicer formulation for the strange mask-changing view shift introMerge branch 'master' of gitlab.mpi-sws.org:FP/iris-coqdocs: move more things to their right place: timeless, persistent; also define and give rules for ghost ownership, view shift, WPRemove superfluous whitespace.Merge branch 'master' of gitlab.mpi-sws.org:FP/iris-coqdocs: complete section on composeable dynamic ghost ownershipFixed typos in the definition of the interpretation of pvs.Merge branch 'master' of gitlab.mpi-sws.org:FP/iris-coqfix some typosAvoid camelcased names.deleted an errant lambdadocs: higher-order ghost state writing