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.015Feb1413121110985432131Jan302927262523222120191817161413129865422Dec21161514118423Nov22201918171612119630Oct2928272316151431Aug16Jul24Jun2215115432131May30292827262516151413establish monotnicity of ownershipsts: define state in terms of states; prove states_fsaprove sts.openingprove sts.opened; state sts.closingprove some properties of discrete CMRAssts: embrace modulesprove sts_alloc; play around with modules and namespaces for stsauth.v: reduce noise by putting definitions in a sectionbasics of Sts constructionsts: change order of S and T to consistently be "S T" (also for consistency with on-paper def.)heap: slightly simplifyMost language notation keywords include a colon: now if does too.Strenghten heap_alloc using big_op.Preliminary version of big_op over uPred for fin_map.Left and right mononicity properties for uPred_and and uPred_or.Remove outdated TODO.Rename from_heap -> of_heap.Remove the primitive for full ownership of a heap.More properties about auth_own.Left and right mononicity properties for uPred_sep.Misc fin_map CMRA properties.Inserting into a fin_map twice.Move uPred big_op stuff to separate file.Heap stuff no longer depends on notations.Change auth_fsa to have an existential quantifier for the update.Merge branch 'master' of gitlab.mpi-sws.org:FP/iris-coqembrace doneMerge branch 'master' of gitlab.mpi-sws.org:FP/iris-coqavoid tricky -{left,right}_id rewritesRename saved_prop_twice -> saved_prop_agree.More consistent fmap and omap properties for fin_maps.Let done do eassumption.port the testcase to use the heap.vcomplete heap.vprove 'strong' allocation of ghost state, with more control over the name that has been pickedstub out the accidentally committed per-location allocationprove compatibility of later and iffprove CAS success caseprove allocthe user can pick some parts of the local update of auth later