Skip to content
Snippets Groups Projects
Select Git revision
  • concur2020
  • cpp21
  • cpp21_deprecated
  • ill
  • iris-update
  • jesper
  • jonas/coexponentials
  • jonas/liter
  • jonas/lty_helper_lemmas
  • jonas/pizza
  • jonas/ring_leader_election
  • lmcs
  • master default protected
  • popl20
14 results
You can move around the graph by using the arrow keys.
Created with Raphaël 2.2.06May54130Apr292524232221181716151413642131Mar2726252416131221Feb1727Nov25242118171615137231Oct25231918171413121110123Sep1722Aug2111Jul109876543130Jun28272625211817121131May29987230Apr292726252319181715121142129Mar2726Make type in shared ref copy.Remove old stuff.Notation for binder_insert.Removed dangling `-` that somehow did not cause compilation errorsfix pair exampleMerge branch 'daniel/update_typing_rules' into 'master'minor refactoring of typing rulesupdate remaining rules, split mutex into libupdate more typing rulesstart updating typing rulesMerge branch 'master' of https://gitlab.mpi-sws.org/iris/actrisFunctional correctness spec of double example.Merge branch 'jonas/more_polymorphism'Revert "Updated variable rule to be in line with paper version"Updated variable rule to be in line with paper versionStronger variable rule.Merge branch 'daniel/copy_derived_rules' into 'master'remove value restriction TODOremove bounded quantificationAdd Löb TODOadd some derived copyability rulesMerge branch 'jonas/more_polymorphism' into 'master'Remove `lty_texist`.Generalize to binder.Tweaks.Tweaks.WIP: Progress on recv ruleDefined conversion functions from ktele to teleWIP: Stated the subtyping rules for texistAdded notation for telescope message typesAttempt at function from ktele to teleWIP: Initial attempt at recv and unpack rulesNitsWIP: Polymorphic rule for receiveNotation nits and fixed subtyping oversightUpdated delete rule and bumped proofsProved new style of let and unpack rulesRevert "Bounded subtyping."NitFixed contractiveness of choice