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.021Sep1716151410874326Aug25212015728Jul24222120152130Jun29195429May28262418131087654130Apr292524232221181716151413642131Mar2726252416131221Feb1727Nov25242118171615137231Oct25231918171413121110123Sep1722Aug2111Jul109876543130Jun28272625211817121131May29987230Apr292726252319181715121142129Mar2726Refactoring of client/serviceReview comments for compute exampleAddressing review commentsAdded example of computation service with producer/consumer clientAdded coercion lemmas for lstyAdded value typing judgement and value rules for lam and recMerge branch 'master' of https://gitlab.mpi-sws.org/iris/actrisRecovered original double manual proofLookup function on env.Environment subtyping rules for copy.RefactoringAdded typing example for uncheckable mapperRemoved redundant monotonicity lemma for typing judgementProved weaker rules of dual/append over send/recv with stronger polymorphic rulesAdded type former for a type appended N timesAdded stronger lemma for framing judgementSubtyping 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)