We present the first higher-order typed functional language that also supports choreographic programming, which allows distributed programs to be written using an “Alice-and-Bob” notation.
Andrew K. Hirsch, Deepak Garg
We present Pirouette, the first language for typed higher-order functional choreographic programming. Pirouette offers programmers the ability to write a centralized functional program and compile it via endpoint projection into programs for each node in a distributed system. Moreover, Pirouette is defined generically over a (local) language of messages, and lifts guarantees about the message type system to its own. Message type soundness also guarantees deadlock freedom. All of our results are verified in Coq.