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.015Mar1197316Feb14121130Jan2925191321Dec161026Nov21171311531Oct3029221913109532130Sep29281587653226Aug23Jul22151098763230Jun191229May2422158724Apr23874231Mar302120181613121193226Feb25242119181715141312117419Jan18131117Dec131093222Nov21128731Oct2221109875425Sep2320191817151413116543231Aug302928272625231613129643131Jul302926252423221711928Jun26201813111065429May2625241615141312229Apr2524314Mar127642128Feb2726222120151211754131Jan3024231587219Dec141021Nov161514874129Oct252420198765430Sep2120191813107653225Aug24222019829Jul282322201913530Jun29282726bump the Coq version we testMerge branch 'ci/ralf/ghostcell' into 'master'more comments explaining the weakened typing ruleadd GhostCell proof by Joshua Yanovskiadd BrandedVec proof by Joshua Yanovskimake external lifetime context inclusion syntactic, and adjust type system and existing proofsadd derived 'meta' mechanism to lifetime logic: associate a lifetime with metadata (via a gname)add 'syntactic' notion of lifetim inclusion and prove basic lemmas about itprove that Skip is atomicupdate dependenciesBumpupdate dependenciesupdate dependenciesBump Iris.add variant of diverging_static for arbitrary invariant lifetime positionsdiverging_static can now be checked in the type systemshow variant of equalization with the static lifetimeupdate dependenciesfix typosfix typo: relf -> reflupdate dependenciesBump Iris.change lemma typecontractivenesscontractivenessfix automation for different notion of contractivenessMerge branch 'master' of gitlab.mpi-sws.org:iris/lambda-rustoption is non-expansive.Merge branch 'master' into gpirlea/pinninggpirlea/pinninggpirlea/pinningremove unused import of hoare moduleupdate dependenciesbump dependencymasters/weak_memmasters/weak_memProve more precise Sync/Send instances for RwLock guards.prove Send instances for lock guardsfix compatibility with latest Coq masterupdate dependenciesfix compatibility with latest Coq masterupdate dependenciesstop testing Coq 8.11update build systemupdate build systemupdate CI config