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
  • fix-class-apply
  • fix-export
  • fix-from-assumption-exact
  • fix-local-inductive
  • instance-nobody-open-proof
  • iris-3.0
  • iris-3.1
  • janno/metacoq
  • jh/done_contradiction
  • 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.016Feb151413121110985432131Jan302927262523222120191817161413129865422Dec21161514118423Nov22201918171612119630Oct2928272316151431Aug16Jul24Jun22151154Big op for uPred_sep for finite sets.define the invariants and assertions we need for the proofdefine the set of low states and prove it closedMove DRA validity instances into section to avoid ambiguity.Merge branch 'master' of gitlab.mpi-sws.org:FP/iris-coqConversion of gset to set.Merge branch 'master' of gitlab.mpi-sws.org:FP/iris-coqbarrier: prove stability of a setsts: for disjointness, it is enough to demand being a subset of the empty setUse unicode not for mkSet_not_elem_of.we also need to go below mkSet for \notinprovide a way to get bbelow mkSetavoid by in tactics (as advised by Robbert)Merge branch 'master' of gitlab.mpi-sws.org:FP/iris-coqprelude.collections: add lemma to prove non-emptinessTweak use of wp_value in wp_tactics.some playing around with wp_tacticsdefine the program we want to verify, and the STS we plan to useSimplify up_set_proper.Rename sts -> stsT.Some test tweaks.Use some wp tactics in heap example.Missing heap_lang ;; notation for values.Use > for wp_tactics that do not strip later.wp_tactics: use wp_value afterwards instead of before.Merge branch 'master' of gitlab.mpi-sws.org:FP/iris-coqPreliminary version of tactics for automatically applying wp rules.Make reshape_expr more robust.Missing heap_lang let: notation for values.turn STSs into a record*finally* arrive at the weakening for STS state asswrtions that we needMerge branch 'master' of gitlab.mpi-sws.org:FP/iris-coqprove that we actually completely characterized inclusion of the STS RA; derive a simpler formGeneralize wp_fork to have an arbitrary post-condition.Put discrete_validI together with the other validIs and shorten its proof.Merge branch 'master' of gitlab.mpi-sws.org:FP/iris-coqStronger saved_prop_agree with equality instead of iff.Add reflexivity for equality to the uPred hint DB.Anti symmetry for sets.complete STS construction