Skip to content
Snippets Groups Projects

Repository graph

You can move around the graph by using the arrow keys.
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
Created with Raphaël 2.2.017Sep16151410874326Aug25212015728Jul24222120152130Jun29195429May28262418131087654130Apr292524232221181716151413642131Mar2726252416131221Feb1727Nov25242118171615137231Oct25231918171413121110123Sep1722Aug2111Jul109876543130Jun28272625211817121131May29987230Apr292726252319181715121142129Mar2726Subtyping rules for polymorphic session typesOops.Separate file for session typing rules.Closed type checking of polymorphic mapper exampleProve also the external version of the amber rule for fixpoints.Fix rec rule.Use list based environment representation.Squashed commit of the following:Remove ◇ in def of ⊑.Merge branch 'master' of https://gitlab.mpi-sws.org/iris/actrisRemoved unused variable from app choice lemmasbump Coq versionupdate dependencies; fix for agree_op renameProof nitsReintroduced contractiveness of lty_choiceUncurried contractiveness of lty_msg_base, and added contractive of lty_chanRemoved later from payloads in session typesMake `ltyped_recv_texist` better suited for `iApply`.Changed rules to use a framed variantUpdated order of typing rulesUpdated typing rules to algorithmic typingBumped Coq 8.12 warning fixesProven Amber-like ruledeny warnings (and bump Coq to 8.11.2)Fix warnings.Merge branch 'master' of https://gitlab.mpi-sws.org/iris/actrisMade list reversal proof in line with mechanisation section proofsync warning settingsupdate dependenciesClean-upAdded list reverse exampleNitsFixed bugsadded branch existance checkjesperjesperProved contractiveness of iProto_own and iProto_mapstoAdded nary choiceNits in subprotocol example proofAdded basic program proof of references in loops with swappingCleaned up a proofAdded flag to prevent warnings from Coq 8.12 bump