Skip to content
Snippets Groups Projects

Repository graph

You can move around the graph by using the arrow keys.
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
Created with Raphaël 2.2.013Jan1211109876543128Dec2625242322212019181716151413121198762130Nov29282726252423221615111098743128Oct272625166316Sep151413121110965226Aug241898421Jul1312118732130Jun272423rename 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.Simplify proof of soundness/adequacy.solve_inG ftwrename soundness -> adequacyI can't make a commit with a new file without forgetting to add it...Merge branch 'master' of gitlab.mpi-sws.org:FP/LambdaRust-coqSoundness of the type system. Also, added a file typing.v that reexports all the type system.lang/heap: do sealing with primitive projectionsMake it possible to nest uninit products for subtyping.Alpha renaming.Have subtyping between product of uninit and uninit automatically proved.More uses of [iDestruct ty_size_eq].Forgot a file.Cleaning : remove hints about [product2] from solve_typing (this type is only for internal use), and removed unnecessary unfold lemmas.Merge branch 'master' of gitlab.mpi-sws.org:FP/LambdaRust-coqTypechecked lazy lifetime initialization. Also, switched from eauto to typeclasses eauto, which seems way less bugged (but I still found something strange...).use the fact that we can specialize lemmas below laterTypechecking unwrap_or.Merge branch 'master' of https://gitlab.mpi-sws.org/FP/LambdaRust-coqprove writing to Cell; tune some notationMerge branch 'master' of gitlab.mpi-sws.org:FP/LambdaRust-coqType-checking option_as_mut.forgot to add cell to _CoqProjecttyping/tests: make all the functions values as they should beProve that Cell<T> is a type and copy if T is copytry and fail to make using ty_size_eq on \later own more convenientawk.Makefile: uninstall .v and .glob filesawk.Makefile: uninstall: also delete empty directoriesfix awk.Makefilehide the lifetime logic CMRAs behind the signature as wellupdate awk.MakefileMerge commit '7726a27bb6ee6b89e1f4333bef098357ca0b8cf0'Trying to clarify priorities of mergeing and splitting lemmas. Clearly, this is still not optimal.Merge branch 'master' of https://gitlab.mpi-sws.org/FP/LambdaRust-coquse solve_inG tacticupdate Iris