DROPS

Document

DOI: 10.4230/LIPIcs.ITP.2026.15

Formalizing a Hoare Calculus for Choreographic Programming

Authors: Luís Cruz-Filipe and Thomas Wulff Heissel

Published in: LIPIcs, Volume 382, 17th International Conference on Interactive Theorem Proving (ITP 2026)

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

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)

Copy BibTex To Clipboard

@InProceedings{cruzfilipe_et_al:LIPIcs.ITP.2026.15,
  author =	{Cruz-Filipe, Lu{\'\i}s and Heissel, Thomas Wulff},
  title =	{{Formalizing a Hoare Calculus for Choreographic Programming}},
  booktitle =	{17th International Conference on Interactive Theorem Proving (ITP 2026)},
  pages =	{15:1--15:18},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-436-9},
  ISSN =	{1868-8969},
  year =	{2026},
  volume =	{382},
  editor =	{Komendantskaya, Ekaterina and Nipkow, Tobias},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2026.15},
  URN =		{urn:nbn:de:0030-drops-269896},
  doi =		{10.4230/LIPIcs.ITP.2026.15},
  annote =	{Keywords: choreographic programming, theorem proving, Hoare calculus}
}

Search Results

Documents authored by Heissel, Thomas Wulff

Formalizing a Hoare Calculus for Choreographic Programming

Abstract

Cite as

Thanks for your feedback!

Could not send message