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.09Oct765428Sep272625212019729Aug28242221191716108432131Jul19171611107643220Jun18May171615131294229Apr282726252422201918141311730Mar28272423222116151310976543128Feb25242322211918171615131211109830Jan262524232221191716131211109876543128Dec2625242322212019181716151413121198762130Nov2928Proof 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 shrREADME: mention minimal opam versionREADME: mention -jMerge branch 'master' of https://gitlab.mpi-sws.org/FP/LambdaRust-coqfix build-dep/opam dependenciesMerge remote-tracking branch 'origin/eq-loc'support MacOSrename CI jobsstrengthen qp_eq_loc; add a testwp_eq_loc: don't throw away the mapstosMerge remote-tracking branch 'origin/master' into eq-locdocument pointer comparison non-determinismupdate awk.Makefileupdate Irisupdate for Coq Makefile hooksupdate Makefile, gitignore