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.031Jul19171611107643220Jun18May171615131294229Apr282726252422201918141311730Mar28272423222116151310976543128Feb25242322211918171615131211109830Jan262524232221191716131211109876543128Dec2625242322212019181716151413121198762130Nov29282726252423221615111098743Put 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-coqAn example with non-lexical lifetimes.explain a weird design choiceUse return: instead of "return".Use type_call_iris to simplify some proofs.Fake a shared cell from a mutable borrow.Fix FIXME.Bump Iris.fix FIXMEfix buildUse new function call lemma in spawn, take_mut