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.09Feb830Jan262524232221191716131211109876543128Dec2625242322212019181716151413121198762130Nov29282726252423221615111098743128Oct272625166316Sep151413121110965226Aug241898421Jul1312118732130Jun272423update iris to use stdppupdate buildsystemuse new function type notation for examplesnotation for the function typeCell::get_mut does not need the type to be copyDereferencing and dropping a RefMut.Forgot to add two files.Merge remote-tracking branch 'origin/master'dropping a ref.Fix compilation with latest Iris.Update the heap construction to use the state interpretation.Dereferencing a ref.Cloning a ref.Move refcell into a folder.Merge branch 'master' of gitlab.mpi-sws.org:FP/LambdaRust-coqrename _iff_proper -> _iffSplit refcell.v into pieces.(Im)mutable borrowing of refcells.Refcell::into_inner.Typecheck refcell::new.Try to stay up to date wrt heaplang's proofmode.v.RefMut is a type.Ref is a type.Tweaking refcell.RefCell is a type.Idem for derived kinds of borrows.Simplify proofs related to unique borrows by making borrows respectfull of iff.Use pattern matching for defining some types. This make some proof simpler.Boxes for function types are part of the function type itself and we do not need to add them everywhere.Cell : cleanup a bit. Transform the various primitices into functions.fix typo in unmk_celldon't register instance twicemoar parallel function.vopam-pins: avoid re-downloading already properly pinned packagesopam-ci: avoid re-downloading already properly pinned packagesrename tests -> exampleschange notation for memcpy. notation for sum injection has a \Sigma.Revert "rename soundness -> adequacy"Merge branch 'master' of gitlab.mpi-sws.org:FP/LambdaRust-coqFix typo.