Mechanizing Choreographic Programs and Hoare Logic with State Transformers
Timon Böhler, Simon Daniel, David Richter, Pascal Weisenburger, Mira Mezini
cs.PL
Aug 17, 2026 · v1
TL;DR
A choreographic language with state transformers is mechanized in Lean, proving endpoint projection soundness, deadlock freedom, confluence, and a Hoare logic.
Abstract
Choreographic programming is a programming model for developing distributed applications where an entire communication protocol is written as a single program, which a compiler then projects to one process per participant. Choreographic programming abstracts over low-level network communication primitives such as sockets, and provides a high degree of safety guarantees with deadlock freedom ensured by construction. Mechanizing choreographies necessarily deals with both operations specific to distributed programming and standard (local) operations that also occur in non-distributed programs, as well as the typical issues of binding and substitution. We aim to sidestep the latter issues, thereby obtaining a more concise mechanization that focuses on the essential distributed aspects of choreographies. To this end, we use a method recently proposed by Thiemann to elegantly model deadlock-free processes in a dependently typed language: Using state transformers to represent the computations performed by each process. We bring the state transformer model to choreographies, allowing us to reduce the usual mechanization effort around binding and substitution, and to abstract over the details of the "local" aspects of the language. We mechanize in Lean a choreographic language that supports point-to-point communication, broadcasting, recursive procedures, and local stateful methods, allowing each participant to be assigned a different set of methods. We prove soundness and completeness of endpoint projection, establish deadlock freedom for the projected processes, prove confluence, and verify a Hoare logic for choreographies.
Problem
Mechanizing choreographic programming languages is complex, largely due to handling variable binding, substitution, and renaming for distributed programs. Existing mechanizations require intricate proof developments dominated by binder management.
Approach
Choreographies are encoded in Lean using state transformers, where each process holds a state of arbitrary type and communication operations are meta-language functions reading/updating state. This avoids variable contexts, binding, and explicit local expression languages by delegating local computation to Lean functions. The language is parametrized via a type class over roles, local states, methods, and procedure identifiers. Hoare logic is defined semantically, representing rules as Lean theorems rather than a deep embedding.
Results
The language supports point-to-point communication, broadcasting, recursive procedures, and role-specific local methods. Soundness and completeness of endpoint projection, deadlock freedom of projected networks, confluence, and a Hoare logic for choreographies were proved in Lean.
