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.022Feb211918171615131211109830Jan262524232221191716131211109876543128Dec2625242322212019181716151413121198762130Nov29282726252423221615111098743128Oct272625166316Sep151413121110965226Aug241898421Jul1312118732130Jun272423bump 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 eqtypeBump 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.Bump Iris and fix stuff.Port Iris 84d78426: Remove an Ltac hack that was there for unknown reason.Merge branch 'master' of https://gitlab.mpi-sws.org/FP/LambdaRust-coqavoid using wp_bind; use wp_apply insteadRemove uses of iStartProof, which is intended as being an internal tactic.Bump iris. Simplify some proofs.refcell: split switching back to the type system and chekcing the first instruction into two stepsupdate Cell to prove replace instead of just set (like in latest nightly Rust)Bump Iris and remove a FIXME.Remove another FIXME.Bump Iris and fix several TODOs and FIXMEs.update lang to use heap_lang style: merge lifting.v and derived.vshow join_handle_subtype inside the logicallow subtyping for join_handlenote a TODOtype the join functionprove that spawn can return a join handlewp_alloc provides a vector of allocated valuesleave a TODOMerge branch 'master' of https://gitlab.mpi-sws.org/FP/LambdaRust-coqadapt the locking approach for value-lambdas like we did in iris.heap_langBumb Iris version.Remove obsolete TODO.prove a spawn-join primitiveupdate build systemMerge branch 'master' of gitlab.mpi-sws.org:FP/LambdaRust-coqIris master.Merge branch 'master' of https://gitlab.mpi-sws.org/FP/LambdaRust-coq