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.013Oct1210976543228Sep272120191514131298765432131Aug302928272625242322212019181716141110986542128Jul272625232221201918161513121165432130Jun2827262524232120191817161514876131MayMerge 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.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 lambda
Loading