Keep me out of the loop: a more flexible choreographic projection

Luís Cruz-Filipe, Fabrizio Montesi, Robert R. Rasmussen [2023].
In proceedings of LPAR 2023, pp. 144-163.

Abstract

Choreographic programming is a paradigm where programmers write global descrip- tions of distributed protocols, called choreographies, and correct implementations are au- tomatically generated by a mechanism called projection. Not all choreographies are pro- jectable, because decisions made by one process must be communicated to other processes whose behaviour depends on them – a property known as knowledge of choice.The standard formulation of knowledge of choice disallows protocols such as third-party authentication with retries, where two processes iteratively interact, and other processes wait to be notified at the end of this loop. In this work we show how knowledge of choice can be weakened, extending the class of projectable choreographies with these and other interesting behaviours. The whole development is formalised in Coq. Working with a proof assistant was crucial to our development, because of the help it provided with detecting counterintuitive edge cases that would otherwise have gone unnoticed.

Links

doi.org

Additional notes

None

Cite (BibTeX)

Click to expand

@inproceedings{DBLP:conf/lpar/Cruz-FilipeMR23,
  author       = {Lu{\'{\i}}s Cruz{-}Filipe and
                  Fabrizio Montesi and
                  Robert R. Rasmussen},
  editor       = {Ruzica Piskac and
                  Andrei Voronkov},
  title        = {Keep me out of the loop: a more flexible choreographic projection},
  booktitle    = {{LPAR} 2023: Proceedings of 24th International Conference on Logic
                  for Programming, Artificial Intelligence and Reasoning, Manizales,
                  Colombia, 4-9th June 2023},
  series       = {EPiC Series in Computing},
  volume       = {94},
  pages        = {144--163},
  publisher    = {EasyChair},
  year         = {2023},
  url          = {https://doi.org/10.29007/wbw3},
  doi          = {10.29007/WBW3},
  timestamp    = {Mon, 03 Mar 2025 21:17:22 +0100},
  biburl       = {https://dblp.org/rec/conf/lpar/Cruz-FilipeMR23.bib},
  bibsource    = {dblp computer science bibliography, https://dblp.org}
}

A PDF is available (possibly a preprint):