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/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
Created with Raphaël 2.2.012Nov119630Oct2928272316151431Aug16Jul24Jun221615115432131May302928272625161514131211723Apr141311109872131Mar30292827252423201918171613121186543228Feb27262423222120191817161514131195432131Jan3024Oct76517Jul1198621Jun2019654331May2928Improved unit for (decidable) agreement RA.Owning a monoid element.Remove type class instances non-expansive -> proper.Now compiles with 8.5 beta 3.Initial commitmake world satisfaction not monotone nor anto-monotone wrt. the resource. that's not a property we want to use anywhere.define operations as plain coq functions rather than non-expansive functions. this signficiantly improves the behavior of 'simpl morph're-establish derived stateful lifting lemmasshow a stronger lifting lemma, that can access invariantsmake weakest-pre trivial again at level 1move the is_ctx definition to core_lang for better visibilityupdate gitignorerename: filling function -> context functionadd a helpful commenttune the filling axioms to make more sensealso show htBind in ectx_langremove commented-out old axiomsrefine filling axioms; add ectx_lang: a language defined in terms of evaluation contexts; show that it can do fillingshow again the general bind ruleoO we can have a general bind rule... with very few assumptions about filling*oops* I renamed that one...update the 'stupid' language in iris_check*oops* make things compile againdone re-establishing liftingcomplete stateful liftingre-establish the stateful liftingreestablish derived HT propertiesreestablish basic HT propertiesremove commented-out axioms; fix weakest-pre and also change it to no longer contain the final view shift; re-establish adequacyfork be gone. iris_meta brokenShow the relationship between safe expressions and thread pool reductionimprove benchmark scriptshow that fork is atomic!weakest pre: forked thread can have full mask. as a result, the fork rule got stronger.agreement: simplify metricMerge branch 'master' of git.fp.mpi-sws.org:nowbookinv is contractiveshow that for AFrame, it is good enough to have any non-valueprove the close relationship between wp on values and non-mask-changing view shiftsshow some things about the magic wand