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.09Oct765428Sep272625212019729Aug28242221191716108432131Jul19171611107643220Jun18May171615131294229Apr282726252422201918141311730Mar28272423222116151310976543128Feb25242322211918171615131211109830Jan262524232221191716131211109876543128Dec2625242322212019181716151413121198762130Nov29A bit of refactoring never hurts.It is not necessary to ask lifetime inclusion to trade dead tokens. A lot of simplifications follow.Fractured borrows.Fix lifetime_sigWeakly synchronized accessor for inat_bor."Weakly synchronized" accessor for indexed borrows. Useful for atomic borrows whose payload synchronizes with the end of the lifetime.fix notation.change the notation for borrows : now, it is just a notation for the predicate transformer (it does not include the payload of the borrow).Internal persistent atomic borrows.Make lft_incl depend on the viewComment.Refactoringidx_bor_own need not be fractionalPut all the view/vPred stuff in infra.vProve derived facts about the lifetime logic.Proof of bor_combine. This completes the (internal part of) the lifetime logic.Make atomic accessor expressible in iGPS, and prove bor_split.Unnesting.Refactoring and simplifications.Creating and ending lifetimes.Creating borrows. Also, proved a few lemmas about semilattices to simplify existing proofs.Accessors : done.Non-atomic accessor for full borrowsAtomic accessor for indexed borrows.Non-atomic accessor for indexed borrows.Fixed (hopefully) atomic accessors, and proved faking a borrow.Add a bottom element to the semilattice structure, plus a bit of refactoring.WIP: fixed the cons accessors, used a notation for vProp in signature. There is some serious TODO left in ilft_create.disable CIWork on primitive.v. Use leibniz equality on view (tedious otherwise), we may or may not need to change that.Work on definitionsInitial commit of the weak branchupdate Makefilemaybe upgrade is less ill-behaved than reinstallremove empty modules filesstop excluding files from git exportsavoid newline in quoted textpopl18-aecpopl18-aecexplain updatingexpand READMEmove sharing lemmas around so that uniq does not depend on shr