Document Open Access Logo

Formalizing a Hoare Calculus for Choreographic Programming

Authors Luís Cruz-Filipe , Thomas Wulff Heissel

PDF

File

Thumbnail PDF
PDF
LIPIcs.ITP.2026.15.pdf
  • Filesize: 0.7 MB
  • 18 pages

Document Identifiers

Subject Classification

ACM Subject Classification
  • Theory of computation → Concurrency
  • Theory of computation → Automated reasoning
Keywords
  • choreographic programming
  • theorem proving
  • Hoare calculus

Metrics

Abstract

Choreographic programming is a paradigm where developers write the global specification (called choreography) of a communicating system, and then a correct-by-construction distributed implementation is compiled automatically. Choreographies formalize the way many practitioners think about distributed protocols, and are a natural framework in which to prove properties of such protocols.
Previous work has introduced a Hoare calculus for reasoning about choreographies. In this article, we show how a formalization of that work in a theorem prover revealed several issues with the pen-and-paper development. We discuss the extent to which these issues can be fixed, and conclude with some considerations on the need for more formal verification of research results.

Cite As Get BibTex

Luís Cruz-Filipe and Thomas Wulff Heissel. Formalizing a Hoare Calculus for Choreographic Programming. In 17th International Conference on Interactive Theorem Proving (ITP 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 382, pp. 15:1-15:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026) https://doi.org/10.4230/LIPIcs.ITP.2026.15

Author Details

Luís Cruz-Filipe
  • IT University Copenhagen, Denmark
Thomas Wulff Heissel
  • Department of Computer Science, University of Southern Denmark, Odense, Denmark

Supplementary Materials

References

  1. Krzysztof R. Apt and Ernst-Rüdiger Olderog. Fifty years of hoare’s logic. Formal Aspects Comput., 31(6):751-807, 2019. URL: https://doi.org/10.1007/S00165-019-00501-3.
  2. Sylvain Boulmé. Tutorial on Hoare logic. URL: https://rocq-prover.org/p/coq-hoare-tut/8.11.1.
  3. Mario Bravetti, Marco Carbone, Julien Lange, Nobuko Yoshida, and Gianluigi Zavattaro. A sound algorithm for asynchronous session subtyping and its implementation. Log. Methods Comput. Sci., 17(1), 2021. URL: https://lmcs.episciences.org/7238.
  4. Mario Bravetti, Marco Carbone, and Gianluigi Zavattaro. Undecidability of asynchronous session subtyping. Inf. Comput., 256:300-320, 2017. URL: https://doi.org/10.1016/j.ic.2017.07.010.
  5. Mario Bravetti, Marco Carbone, and Gianluigi Zavattaro. On the boundary between decidability and undecidability of asynchronous session subtyping. Theor. Comput. Sci., 722:19-51, 2018. URL: https://doi.org/10.1016/j.tcs.2018.02.010.
  6. Marco Carbone and Fabrizio Montesi. Deadlock-freedom-by-design: multiparty asynchronous global programming. In Roberto Giacobazzi and Radhia Cousot, editors, Procs. POPL, pages 263-274. ACM, 2013. URL: https://doi.org/10.1145/2429069.2429101.
  7. David Castro-Perez, Francisco Ferreira, Lorenzo Gheri, and Nobuko Yoshida. Zooid: a DSL for certified multiparty computation: from mechanised metatheory to certified multiparty processes. In Stephen N. Freund and Eran Yahav, editors, Procs. PLDI, pages 237-251. ACM, 2021. URL: https://doi.org/10.1145/3453483.3454041.
  8. Luís Cruz-Filipe, Eva Graversen, Fabrizio Montesi, and Marco Peressotti. Reasoning about choreographic programs. In Sung-Shik Jongmans and Antónia Lopes, editors, COORDINATION 2023, volume 13908 of Lecture Notes in Computer Science, pages 144-162. Springer, June 2023. URL: https://doi.org/10.1007/978-3-031-35361-1_8.
  9. Luís Cruz-Filipe and Fabrizio Montesi. Procedural choreographic programming. In Ahmed Bouajjani and Alexandra Silva, editors, Procs. FORTE, volume 10321 of Lecture Notes in Computer Science, pages 92-107. Springer, 2017. URL: https://doi.org/10.1007/978-3-319-60225-7_7.
  10. Luís Cruz-Filipe and Fabrizio Montesi. A core model for choreographic programming. Theor. Comput. Sci., 802:38-66, 2020. URL: https://doi.org/10.1016/j.tcs.2019.07.005.
  11. Luís Cruz-Filipe and Fabrizio Montesi. Now it compiles! certified automatic repair of uncompilable protocols. In Adam Naumowicz and René Thiemann, editors, ITP 2023, volume 268 of LIPIcs, pages 11:1-11:19. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, July 2023. URL: https://doi.org/10.4230/LIPIcs.ITP.2023.11.
  12. Luís Cruz-Filipe, Fabrizio Montesi, and Marco Peressotti. Certifying choreography compilation. In Antonio Cerone and Peter Csaba Ölveczky, editors, Procs. ICTAC, volume 12819 of Lecture Notes in Computer Science, pages 115-133. Springer, 2021. URL: https://doi.org/10.1007/978-3-030-85315-0_8.
  13. Luís Cruz-Filipe, Fabrizio Montesi, and Marco Peressotti. Formalising a Turing-complete choreographic language in Coq. In Liron Cohen and Cezary Kaliszyk, editors, Procs. ITP, volume 193 of LIPIcs, pages 15:1-15:18. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2021. URL: https://doi.org/10.4230/LIPIcs.ITP.2021.15.
  14. Luís Cruz-Filipe, Fabrizio Montesi, and Marco Peressotti. A formal theory of choreographic programming. Journal of Automated Reasoning, 67(2):21:1-21:34, May 2023. URL: https://doi.org/10.1007/s10817-023-09665-3.
  15. Luís Cruz-Filipe, Fabrizio Montesi, and Robert R. Rasmussen. Keep me out of the loop: a more flexible choreographic projection. In Ruzica Piskac and Andrei Voronkov, editors, LPAR 2023, volume 94 of EPiC Series in Computing, pages 144-163. EasyChair, June 2023. URL: https://doi.org/10.29007/WBW3.
  16. Luís Cruz-Filipe and Thomas Wulff Heissel. Formalizing a Hoare calculus for choreographic programming, May 2026. URL: https://doi.org/10.5281/zenodo.20290519.
  17. Mila Dalla Preda, Maurizio Gabbrielli, Saverio Giallorenzo, Ivan Lanese, and Jacopo Mauro. Dynamic choreographies: Theory and implementation. Log. Methods Comput. Sci., 13(2), 2017. URL: https://doi.org/10.23638/LMCS-13(2:1)2017.
  18. Whitfield Diffie and Martin E. Hellman. New directions in cryptography. IEEE Trans. Inf. Theory, 22(6):644-654, 1976. URL: https://doi.org/10.1109/TIT.1976.1055638.
  19. Alain Finkel and Étienne Lozes. Synchronizability of communicating finite state machines is not decidable. In Ioannis Chatzigiannakis, Piotr Indyk, Fabian Kuhn, and Anca Muscholl, editors, Procs. ICALP, volume 80 of LIPIcs, pages 122:1-122:14. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2017. URL: https://doi.org/10.4230/LIPIcs.ICALP.2017.122.
  20. Andrew K. Hirsch and Deepak Garg. Pirouette: higher-order typed functional choreographies. Proc. ACM Program. Lang., 6(POPL):1-27, 2022. URL: https://doi.org/10.1145/3498684.
  21. C.A.R. Hoare. An axiomatic basis for computer programming. Commun. ACM, 12(10):576-580, 1969. URL: https://doi.org/10.1145/363235.363259.
  22. The Iris project. URL: https://iris-project.org/.
  23. Jules Jacobs, Stephanie Balzer, and Robbert Krebbers. Multiparty GV: functional multiparty session types with certified deadlock freedom. Proc. ACM Program. Lang., 6(ICFP):466-495, 2022. URL: https://doi.org/10.1145/3547638.
  24. Sung-Shik Jongmans and Petra van den Bos. A predicate transformer for choreographies - computing preconditions in choreographic programming. In Ilya Sergey, editor, Procs. ESOP, volume 13240 of Lecture Notes in Computer Science, pages 520-547. Springer, 2022. URL: https://doi.org/10.1007/978-3-030-99336-8_19.
  25. Donnacha Oisín Kidney, Zhixuan Yang, and Nicolas Wu. Algebraic effects meet hoare logic in cubical agda. Proc. ACM Program. Lang., 8(POPL):1663-1695, 2024. URL: https://doi.org/10.1145/3632898.
  26. Aleksandar Kupusinac and Dusan Malbask. Formalization of the general hoare logic laws. TEM Journal, 1(3):145-150, 2012. Google Scholar
  27. Julien Lange and Nobuko Yoshida. On the undecidability of asynchronous session subtyping. In Javier Esparza and Andrzej S. Murawski, editors, Procs. FOSSACS, volume 10203 of Lecture Notes in Computer Science, pages 441-457, 2017. URL: https://doi.org/10.1007/978-3-662-54458-7_26.
  28. Tanakorn Leesatapornwongsa, Jeffrey F. Lukman, Shan Lu, and Haryadi S. Gunawi. Taxdc: A taxonomy of non-deterministic concurrency bugs in datacenter distributed systems. In Tom Conte and Yuanyuan Zhou, editors, Procs. ASPLOS, pages 517-530. ACM, 2016. URL: https://doi.org/10.1145/2872362.2872374.
  29. Alberto Lluch-Lafuente, Flemming Nielson, and Hanne Riis Nielson. Discretionary information flow control for interaction-oriented specifications. In Narciso Martí-Oliet, Peter Csaba Ölveczky, and Carolyn L. Talcott, editors, Logic, Rewriting, and Concurrency, volume 9200 of Lecture Notes in Computer Science, pages 427-450. Springer, 2015. URL: https://doi.org/10.1007/978-3-319-23165-5_20.
  30. Hugo A. López and Kai Heussen. Choreographing cyber-physical distributed control systems for the energy sector. In Ahmed Seffah, Birgit Penzenstadler, Carina Alves, and Xin Peng, editors, Procs. SAC, pages 437-443. ACM, 2017. URL: https://doi.org/10.1145/3019612.3019656.
  31. Hugo A. López, Flemming Nielson, and Hanne Riis Nielson. Enforcing availability in failure-aware communicating systems. In Elvira Albert and Ivan Lanese, editors, Procs. FORTE, volume 9688 of Lecture Notes in Computer Science, pages 195-211. Springer, 2016. URL: https://doi.org/10.1007/978-3-319-39570-8_13.
  32. Petar Maksimovic and Alan Schmitt. HOCore in Coq. In Christian Urban and Xingyuan Zhang, editors, Procs. ITP, volume 9236 of Lecture Notes in Computer Science, pages 278-293. Springer, 2015. URL: https://doi.org/10.1007/978-3-319-22102-1_19.
  33. Fabrizio Montesi. Choreographic Programming. Ph.D. Thesis, IT University of Copenhagen, 2013. URL: http://www.fabriziomontesi.com/files/choreographic_programming.pdf.
  34. Johannes Åman Pohjola, Alejandro Gómez-Londoño, James Shaker, and Michael Norrish. Kalas: A verified, end-to-end compiler for a choreographic language. In June Andronick and Leonardo de Moura, editors, Procs. ITP, volume 237 of LIPIcs, pages 27:1-27:18. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2022. URL: https://doi.org/10.4230/LIPIcs.ITP.2022.27.
  35. Alceste Scalas and Nobuko Yoshida. Less is more: multiparty session types revisited. Proc. ACM Program. Lang., 3(POPL):30:1-30:29, 2019. URL: https://doi.org/10.1145/3290343.
  36. Dawit Legesse Tirore, Jesper Bengtson, and Marco Carbone. Multiparty asynchronous session types: A mechanised proof of subject reduction. In Jonathan Aldrich and Alexandra Silva, editors, Procs. ECOOP, volume 333 of LIPIcs, pages 31:1-31:30. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2025. URL: https://doi.org/10.4230/LIPIcs.ECOOP.2025.31.
Any Issues?
X

Feedback on the Current Page

CAPTCHA

Thanks for your feedback!

Feedback submitted to Dagstuhl Publishing

Could not send message

Please try again later or send an E-mail
© 2023-2026 Schloss Dagstuhl – LZI GmbH Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact