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.028Mar272423222116151310976543128Feb25242322211918171615131211109830Jan262524232221191716131211109876543128Dec2625242322212019181716151413121198762130Nov29282726252423221615111098743128Oct272625166316Sep151413121110965226Aug241898421Jul1312118732130Jun272423Remove 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 fixedMerge branch 'fnlft' of gitlab.mpi-sws.org:FP/LambdaRust-coq into fnlftWIP.WIP: new function rules doneWIP sum: prove subtypingWIP.WIP: "Lifetime of a function" instead of liveness assumptions in external lifetime contextBump Iris.Remove 'Typeclasses Opaque' that were inside a section and hence ineffectiveUse `max_list_with` from std++.Update Iris.Update to latest Iris.Simplify a proofUse new destruct for bigopsupdate to latest Irisfix fallout of new bigops stuff in Iristhis should be right version of Irisexperiment with some lemmas to help reduce boilerplate in unsafe code proofsfix buildupdate Irisproof script prettification