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.06Mar543128Feb25242322211918171615131211109830Jan262524232221191716131211109876543128Dec2625242322212019181716151413121198762130Nov29282726252423221615111098743128Oct272625166316Sep151413121110965226Aug241898421Jul1312118732130Jun272423Try making [lrust_typing] non-discriminated to see whether anything changes.Tweak.Merge branch 'master' of gitlab.mpi-sws.org:FP/LambdaRust-coqFaking a shared box.Make solve_typing able to solve [typed_read] and [typed_write].lrust_typing: make sum type opaque, for consistency with the other typesfix comment in spawn.vMerge branch 'ralf/ci/box' into 'master' Fix [solve__typing] by changing the hint on [tctx_extract_hasty_here_eq] into a [Hint Resolve], so that the opaqueness annotations are not ignored.Make box a definition and prove it contractiveNew notation : typed_val.bump Irisswitch to new CI machineforgot to bump Irismake join_handle a contractive typeshow all type-non-expansive functions to also be properly non-expansivenew fixpointClarify the API of shared borrows: create specific lemmas for lftN.Use the empty set for the mask of the closing update of borrows.Dynamic masks for lifetimes.jh/dynamic_masksjh/dynamic_masksProove that RWlock is safe.Cosmetic changes in refcell.Change the masks of shared borrows, so that the previous commit has a purpose.Make it possible to specify a namespace for shared borrows.Cosmetic changes in spawn.v.Remove a file from _Coqproject.Define the type option. Merge some examples in this file.bump Iristry to improve parallelism by putting the examples lastMerge branch 'master' of https://gitlab.mpi-sws.org/FP/LambdaRust-coqremove lft_ctx from subtype and eqtypeUse fast_string.fast_stringfast_stringBump Iris.RefCell: add comments explaining the data layoutMap for refmut.Map for Ref.Make (most of) the typing lemmas implications in Iris.Oops, forgot to bump Iris.Use Iris' iso_ofe infrastructure for types and seal off equiv and dist.Bump Iris version and make use of improved solve_ndisj.