Skip to content
Snippets Groups Projects
Select Git revision
  • channel_closure_spec
  • close_spec
  • concur2020
  • cpp21
  • cpp21_deprecated
  • iris-update
  • jesper
  • jonas/coexponentials
  • jonas/liter
  • jonas/log_atom_2
  • jonas/lty_helper_lemmas
  • jonas/pizza
  • jonas/ring_leader_election
  • later_strip
  • lmcs
  • master default protected
  • mini_actris1
  • miniactris-init
  • mixed_choice
  • mixed_choice_list
20 results
You can move around the graph by using the arrow keys.
Created with Raphaël 2.2.05Feb231Jan302820Nov65Oct4331Aug422May214218Apr20Mar97611Feb629Nov211817Aug161245Jul24Jun717May141312119876125Apr20191228Mar2220Jan10Dec98765Nov2Oct31Aug30262528Jul272029Jun17161454328May19330Apr2025Mar1219Feb1726Jan251116Dec1495227Nov25242317131211428Oct272625211210530Sep292322211716151410874326Aug25212015728Jul24222120152130Jun29195429May28262418131087654130Apr292524232221181716151413642131Mar2726252416131221Feb1727Nov25242118171615137231Oct252319181714131211More cleanupSome cleanupAdded valid targets to consistency relation and removed diverges[list_to_set $ seq] -> [set_eq]Added forwarder exampleImproved new_chan spec and closed example proofsProved new_chan spec (but add a stronger side-condition)Proved admitted ghost lemmaProved example using recursive protocolAdded recursive exampleTwo Buyer Ref protocolAdded two_buyer protocolMore automationAutomation for proving consistency relationMade proofmode resolve idx unificationProofmode!!Bumped subprotocol typeclassesAdded get_chan primitiveSubprotocols doneUpdated subprotocol definition and proved lemmasProved subprotocol lemmasAdded example with resource transferUpdated definition of new_chanHid the channel index on the channel ownershipFirst closed proof!Added multi channels and moreWIP multi_channelProof of concept for synchronous resource transferMoved examples to other file. Added naive def of iProto_leSolve remaining admitsAdded proof of consistency for roundtrip exampleProved ghost theory stepping relationWrapped up API for multiparty ghost theoryWIP: Proof of iProto_consistent_stepWIP: Multiparty definitionSynchronous ghost theory for binary session typesBump Coq 8.19Merge branch 'ci/coq' into 'master'bump to Coq 8.18update dependencies