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.018Apr141311730Mar28272423222116151310976543128Feb25242322211918171615131211109830Jan262524232221191716131211109876543128Dec2625242322212019181716151413121198762130Nov29282726252423221615111098743128Oct272625166316Sep151413121110965226Aug241898421Jul1312118732130Jun272423Weak references : upgrade, downgrade, clone.Begining the work on weak references in Rc: redesign the protocol, define the weak type, and update the code for rc.Typechecking Ralf's example.jh/typecheck_foojh/typecheck_fooMerge branch 'master' of gitlab.mpi-sws.org:FP/LambdaRust-coqBump Iris.use lock_proto only under a laterremove a file I added accidentallyswitch lock spec to be accessor-basedlock allows applying equivalencesupdate Iris; tweak lock a littleslight proof tweaksOops, fix previous commit.Merge branch 'master' of gitlab.mpi-sws.org:FP/LambdaRust-coqBump Iris, fix some stuff.Fix a broken notation.make the lock cancellableimplement a spin lockMove some things from lang/ to lang/lib/Bump Iris and fix some stuff.Fix issues with notations not being pretty printed.Remove redefined list notations in scopes.Misc big op tweaks.Avoid set_solver in favor of solve_ndisj.Update to new big ops in Iris.Attempt at modeling closures. this does not work because of higherjh/closuresjh/closurescommentMerge remote-tracking branch 'origin/fnlft'Line breaks, tweaks.TyWf typeclass for describing lifetime constraints derived from the syntactic structure of types.subtyping for RcRc is type contractiveWIP.fixed Rc, CellWIP.WIP.WIP.fix spawn and cellAdd lemma [lctx_lft_alive_external], which is useful for automation.WIP work on option.vWIP type_sum fixed