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.010Oct976543228Sep272120191514131298765432131Aug302928272625242322212019181716141110986542128Jul272625232221201918161513121165432130Jun2827262524232120191817161514876131May30292827docs: 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 lambdadocs: higher-order ghost state writingsoundness -> consistencydocs: strengthen equality elimination to match what we have in Coqdocs: fix using the fixpoint for WPexplain a little about masksdocs: define the program logicProve correctness of counter with contributions.New notion of local updates.docs: remind reader what the unit symbol meansdocs: intro rule for boxMerge branch 'master' of gitlab.mpi-sws.org:FP/iris-coqdocs: derived PL WIPMore properties about Some _ ≼ Some _.Prove that the dec_agree CMRA is total.Merge branch 'master' of gitlab.mpi-sws.org:FP/iris-coqdescribe how we obtian the dynamic modular higher-order ghost stateProve soundness result as stated in the appendix.docs: update semantic entailmentMerge branch 'master' of gitlab.mpi-sws.org:FP/iris-coqdocs: move proof theory to a single-assumption contextInternalized versions of the equality on funC and morC.Use apply: in iRewrite.IntoOp and FromOp instances for the authoritative fragment.No longer put proof mode class instances in their own file.Get rid of IntoAssert class.Functor for function space cofes.Define FromOp type class and use it in the proof mode.Fix the lemma Some_included' for total CMRAs.tweak the Qp lemmasdocs: update modelappendix: base logic is now up-to-date
Loading