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.022Mar2116151310976543128Feb25242322211918171615131211109830Jan262524232221191716131211109876543128Dec2625242322212019181716151413121198762130Nov29282726252423221615111098743128Oct272625166316Sep151413121110965226Aug241898421Jul1312118732130Jun272423WIP.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 prettificationUpdate to latest Iris.prove Rc::try_unwrapadd Rc::try_unwrap codeMerge branch 'master' of https://gitlab.mpi-sws.org/FP/LambdaRust-coqchange 'cont:' syntax to have explicit binderMake type_jump easier to use by not having to give it the list of parameters.Prove weakening lemmas for elctx_sat.note what is still missing for RcRc::get_mutmake it so that we can give the option type (instead of the list of variants) to the type_sum lemmasRc::drop*oops* undo accidental changesRc::drop codeMerge branch 'master' of https://gitlab.mpi-sws.org/FP/LambdaRust-coq