Pirouette: Higher-Order Typed Functional Choreographies

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.

Publication History

To Appear in POPL 2022


Official Version

Coming Soon

Technical Report

%d bloggers like this: