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.017Aug16108432131Jul19171611107643220Jun18May171615131294229Apr282726252422201918141311730Mar28272423222116151310976543128Feb25242322211918171615131211109830Jan262524232221191716131211109876543128Dec2625242322212019181716151413121198762130Nov29282726252423221615111098Get 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::joinrenameAdd .gitattribute to ignore some files during the export.Anonymize.better explanation what goes on in panic.vREADMESimplify the model of mutexes by removing the exclusive token.SimplificationsMerge branch 'master' of gitlab.mpi-sws.org:FP/LambdaRust-coqDerive unnesting and reborrowing from a common principle.Bump Iris.Lifetime logic: rename shared borrows to atomic (persistent) borrowsMerge branch 'master' of gitlab.mpi-sws.org:FP/LambdaRust-coqComment on function type.expand on a commentMake emp be defined as the empty sum. Make panic return the empty type.Do not allow na reads and CAS to race on the same location.strong_cas_failstrong_cas_failMerge branch 'master' of gitlab.mpi-sws.org:FP/LambdaRust-coq