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.012May119876125Apr20191228Mar2220Jan10Dec98765Nov2Oct31Aug30262528Jul272029Jun17161454328May19330Apr2025Mar1219Feb1726Jan251116Dec1495227Nov25242317131211428Oct272625211210530Sep292322211716151410874326Aug25212015728Jul24222120152130Jun29195429May28262418131087654130Apr292524232221181716151413642131Mar2726252416131221Feb1727Nov25242118171615137231Oct25231918171413121110123Sep1722Aug2111Jul109876543130Jun282726252118171211publish opam packagesmake license machine-readableMade opam file pass lintingbump the Coq we testProved some helper lemmasProven iProto_le_recvLifted ghost theory to new consistency definition - Still needs subprot lemmasAdded description/discussion about current definitionClean up of definitionAdded alternative to example proofSolved NonExpansiveness of new consistencynormalize OCaml versionsconvert iProto_le_send to the new definition of subtypingmake ocaml version explicitProved that iProto_consistent always holds for dual protocolsAdded helper lemmas for [iProto_consistent]NitsAdded example of iProto_consistent proofStart work on proto_consistent for binary session typesmerged branchAdded priotity to swap rule of proofmode to avoid looping TC searchwork workFixed wrong argument scope and clean upclose_specclose_specClosed proof of exclusivity of iProto_ownCleaned up superfluous lemmaProved send_end_inv lemma for deriving contradictionWIP: Added close spec with outstanding admitted lemmasMerge branch 'later_strip' into 'master'Removed `skipN` instruction in `send` implementationRebase and nitslater_striplater_stripLeveraged a stronger `wp_lb_init` specRemoved `skipN` instruction in `send` implementationBump Iris.Fix typo.Remove unused strange lemmas.Avoided use of [apply:] as Coq it caused 8.15.0 looping behaviourIncluded new channel closure file..channel_closure…channel_closure_specMade a closure-based spec for channelswork on well foundnessupdate the well-formedness of local types