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.013Jan1211109876543128Dec2625242322212019181716151413121198762130Nov29282726252423221615111098743128Oct272625166316Sep151413121110965226Aug241898421Jul1312118732130Jun272423opam-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.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 tactic