Skip to content
Snippets Groups Projects
Select Git revision
  • ci/janno/reduction_no_check
  • ci/places
  • ci/pm_red
  • ci/ralf/const-rf
  • ci/ralf/lia-experiment
  • ci/ralf/old-timing-data
  • ci/ralf/sections
  • ci/robbert/faster_iDestruct2
  • ci/robbert/iprop_structures
  • ci/robbert/merge_sbi
  • ci/robbert/merge_sbi_new
  • ci/robbert/merge_sbi_new_weak
  • ci/robbert/merge_sbi_weak
  • ci/robbert/naive_solver
  • ci/weak_mem
  • contractiveness
  • coqbug/match
  • fast_string
  • ghostcell
  • gpirlea/pinning
  • RBrlx-POPL20-artifact
  • popl18
  • popl18-aec
23 results
You can move around the graph by using the arrow keys.
Created with Raphaël 2.2.020Sep19729Aug28242221191716108432131Jul19171611107643220Jun18May171615131294229Apr282726252422201918141311730Mar28272423222116151310976543128Feb25242322211918171615131211109830Jan262524232221191716131211109876543128Dec2625242322212019181716151413121198762130Nov29282726252423coqchk is brokenRemove workaround.update Iris; get rid of opam.pinsAdding iris atomicMerge branch 'master' of mpisws-gitlab:FP/lambdarust-coqAdding location equality.It is not necessary to ask lifetime inclusion to trade dead tokens.jh/lifetime_no_…jh/lifetime_no_dead_tradeadd missing fileshow that we can covnert 'a to 'static if the function never returnsIdem for the types of shared and unique borrows.Change the notation for borrows : now, it is just a notation for the predicate transformer (it does not include the payload of the borrow).no longer test Coq 8.6; start testing 8.7update Irisupdate CI to templates; test against 8.6.1Simplify proofsThe inheritance of raw reborrowing is not (no longer) necessary. Let's remove it and call it shorten.Get rid of down_close in creation.v : we can take all the lifetimes that are alive, which is simpler.Be more coherent in lft_kill by naming K and K' the same way they are named in lfts_killGet rid of lft_inv_alive_twice, which was completely artificial.Rearranging lifetime.v. Changing the proof of bor_unnest: we do not need atomic accessors here.Use notations.Spurious imports.These are spurious laters.These EqDecision instances are not needed.Cleaning up the lifetime logic.Put the internal namespace definitions of the lifetime logic in the model.Put the shift_loc notation in the right scope so that it is parsed/printed properly even when appearing in expressions.Notation for shift_loc (finally \!).Tactical support for null comparison.Merge branch 'master' of gitlab.mpi-sws.org:FP/LambdaRust-coqMake valid comparisons between pointers and 0.unfix a FIXMEadd a note about the arc protocol so that it does not get lostFix a FIXME.Fix lines lenght.fix a commentprove rayon::joinadd comment to spawn verificationadd a stub for rayon::joinrename