Search papers, labs, and topics across Lattice.
This paper introduces a mechanization of choreographic programming using state transformers within a dependently typed language, specifically Lean, to streamline the development of distributed applications. By focusing on the essential distributed aspects and minimizing the complexity of binding and substitution, the authors achieve a concise representation of choreographies that ensures deadlock freedom and soundness. The results include the mechanization of a choreographic language capable of supporting various communication methods and the formal verification of key properties such as confluence and a Hoare logic for choreographies.
State transformers can simplify the mechanization of distributed programming, ensuring deadlock freedom while abstracting away local complexities.
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.
