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.031Oct292726252422212019181312111075432130Sep27262019181210331Aug3029241713112131Jul242319181713976543230Jun2928262523222120191817161514131211109876543131May302928272524232018171514111098743230Apr2928272625242322212019181211109654331Mar30282724Document `state_interp` and `fork_post`.Remove non-fork versions of pure lifting lemmas.Fine-grained post-conditions for forked-off threads.Merge branch 'robbert/fupd_new_axioms' into 'master'Get rid of useless IntoVal uses.New lemma `step_fupdN_wand`, and use instead of `step_fupdN_mono`.Adapt adequacy of total weakest preconditions to use adequacy of fupd.Allow introduction of `∀` under `|={E1,E2}=>` in case the predicate is plain.Document new fupd+plainly laws.Comment about BiFUpdPlainly and affine BIs.A more principled set of axioms for fupd+plainly.Merge branch 'value_constructor' into 'master'Add comment; fix test tests/heap_lang.v.Changelog.wp_pures.Move `Atomic`, `IntoVal` and `AsVal` instances to lifting.Automate proofs of `Atomic` instances.A specific constructor for injecting values in expressionsShow that bupd entails plausibly.robbert/plausiblyrobbert/plausiblyThe plausibly modality.Remove basic updates from the Iris model, and define them using plainly.robbert/bupd_be…robbert/bupd_be_goneSome missing parameters.Some useful BI derived lemmas.Bump Coq 8.8.1 to 8.8.2 in CI.Bump Mtac2-8.8 commit.Revert "Disable 8.7 CI job."Bump Mtac2-8.7 commit.Remove spurious type annotations (there is a `Implicit Type` here).Close issue #218.Disable 8.7 CI job.Fix error resulting from goal_dep merge.Bump Mtac2-8.7 commit.Bump Mtac2-8.8 commit.Do not always call vm_compute for `change_dep`.Prepare code for change to dep. goal type.Bump Mtac2-8.8 commit.For the timing jobs, build our own ocamlProve `E2 ⊆ E1 → P ={E1,E2}=∗ P`.Notation `P ={E1,E2}▷=∗^n Q`.Bump Mtac2-8.8 commit.