Skip to content
Snippets Groups Projects

Repository graph

You can move around the graph by using the arrow keys.
Select Git revision
  • ci/debug
  • ci/for_proph
  • ci/hai/siProp
  • ci/janno/strict-tc-resolution
  • ci/ralf/Z_of_nat
  • ci/ralf/bi-language
  • ci/ralf/frame-frac
  • 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
  • ci/robbert/merge_sbi
  • ci/robbert/naive_solver
  • 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
34 results
Created with Raphaël 2.2.017Feb16151413121110985432131Jan302927262523222120191817161413129865422Dec21161514118423Nov222019181716121196Misc map_to_list properties.sts_ownS_op: fix stupid typoMerge branch 'master' of gitlab.mpi-sws.org:FP/iris-coqderive sts_op_frag from a generic DRA propertyShorten sts_ownS_op.sts_ownS_opwork on newchan_specestablish that saved propositions are AlwaysStablemore flexible masks for sts_alloc and heap_allocstrengthen sts_alloc and auth_allocsome helpful lemmas relating pvs and wandbarrier: Apply ndisj automation, and assume disjointness only where neededadd some automation related to disjointness of namespaceswp_value_pvsauth: more precise commentsUse scheme - then + then * for bullets.Use {[_ := _]} for singleton map so we can use ↦ for maps to.Type class for ⊤ to get overloaded notation for entire set.Move namespace stuff to separate file.Use Disjoint type class to get nice notation for ndisjoint.Use bundled type classes for ghost ownership.Remove FIXME in list_encode_suffix_eq.progress on signal_specintroduce a notion of disjoint namespaces, and prove a few lemmas about itprelude: missing lemmas about inj2; deduce list equality from list encodingadd a comment about the OFE vs COFE situationadd some basic theory about pointwise updates of total functionsbarrier: change invariant such that the mapsto can be obtained without case distinctionstart working on the singal proofstrengthen auth and heap rules to only require the assertion under a laterconsistently call the saved assertions 'R'fix invariant of low statescomplete writing down the invariant of the barrier protocolFix pretty printing of big op notations.Use keywords in the notation of big ops on uPred.Many STS tweaks:Add saved_props to _CoqProject.Merge branch 'master' of gitlab.mpi-sws.org:FP/iris-coqstate the theorem we want to proveMerge branch 'master' of gitlab.mpi-sws.org:FP/iris-coq