Skip to content
Snippets Groups Projects
Select Git revision
  • ci/ike/frame_exist
  • ci/janno/reduction_no_check
  • ci/janno/strict-tc-resolution
  • ci/pinning
  • ci/places
  • ci/pm_red
  • ci/ralf/const-rf
  • ci/ralf/sections
  • ci/weak_mem protected
  • coqbug/match
  • ghostcell
  • gpirlea/pin_semantic
  • gpirlea/pinning
  • jh/closures
  • jh/dynamic_masks
  • jh/lifetime_no_dead_trade
  • jh/typecheck_foo
  • master default protected
  • masters/rusthornbelt protected
  • masters/weak_mem protected
  • 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.09Oct765428Sep272625212019729Aug28242221191716108432131Jul19171611107643220Jun18May171615131294229Apr282726252422201918141311730Mar28272423222116151310976543128Feb25242322211918171615131211109830Jan262524232221191716131211109876543128Dec2625242322212019181716151413121198762130Nov2928272625Fixed (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, gitignoreupdate Irisupdate build systemupdate READMEcoqchk 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_trade