Thomas Wulff Heissel

Formalizing a Hoare Calculus for Choreographic Programming

2026 · University of Southern Denmark Research Portal (University of Southern Denmark)

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 …