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.05Feb231Jan302820Nov65Oct4331Aug422May214218Apr20Mar97611Feb629Nov211817Aug161245Jul24Jun717May141312119876125Apr20191228Mar2220Jan10Dec98765Nov2Oct31Aug30262528Jul272029Jun17161454328May19330Apr2025Mar1219Feb1726Jan251116Dec1495227Nov25242317131211428Oct272625211210530Sep292322211716151410874326Aug25212015728Jul24222120152130Jun29195429May28262418131087654130Apr292524232221181716151413642131Mar2726252416131221Feb1727Nov25242118171615137231Oct25231918171413121110123Sep1722Aug2111Jul109Updated 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 dependenciesImproved fork_chan proofmodeAligned fork_chan tactic binders with protocolsRenamed start_chan to fork_chan to conform with LinearActrisOpened proto scope to avoid superfluous delimitersBasic tactic support for resolving new_chanBumped opam file to new Iris versionBumped Irisupdate readmeupdate dependenciesupdate dependenciesRevert "stick to 8.17 for nightly testing for now"Tweak proof so it does not run into https://github.com/coq/coq/issues/18126 on Coq 8.18.stack on 8.17 for nightly testing for nowupdate dependenciesupdate dependenciesBump Iris (iIntros starts proof).Nitsstep_protostep_protoRemoved redundant conjunctBumped step mod changes, and added session escrow pattern