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.013May1294229Apr282726252422201918141311730Mar28272423222116151310976543128Feb25242322211918171615131211109830Jan262524232221191716131211109876543128Dec2625242322212019181716151413121198762130Nov29282726252423221615111098743128Oct272625166316Sep1514131211Bump Iris.fix FIXMEfix buildUse new function call lemma in spawn, take_muttune ty_own simplification behavior; make uninit.(ty_own) compute the right wayMerge branch 'master' of https://gitlab.mpi-sws.org/FP/LambdaRust-coqshould fix the errorkeep building as many files as possibleFix use of iInduction, we had to generalize first.fix compile*oops* did not mean to commit this yetLemma to call a rust-typed function from IrisMerge commit '3f39048dec610092e963c74c8995eee456cb0328'Remove obsolete FIXME.notationsnotationsRemove a bunch of uses of lock that are no longer needed after 3f39048d.make the static dispatch for closures look more like it looks in RustTurn CNT into a context in the notation.Start working on notations for typing judgments.Printing boxes for let, ;; and letcont.Make ty_own simpl nomatch to avoid many matches in proof states.Delimit scopes of list variants of subst.Fix another FIXME.Bump Iris, fix FIXME.swapUse a "static dispatch" way of presenting higher order functions.prove take_mutArc commentsMutex and MutexGuard subtyping. This completes the Mutex proof.MutexGuard Sync boundMerge branch 'master' of https://gitlab.mpi-sws.org/FP/LambdaRust-coqMutex: Send+SyncMerge branch 'master' of gitlab.mpi-sws.org:FP/LambdaRust-coqweak_count and strong_count for Arc.refine comments even morerefine commentsGuards for rwlock are sync.Merge branch 'master' of gitlab.mpi-sws.org:FP/LambdaRust-coqarc_make_mut.TODO commentssimplification of ty_own is now fairly well-behaved, remove a TODO