Pirouette: Higher-Order Typed Functional Choreographies

TL;DR

Pirouette is a typed higher-order functional choreographic language that enables centralized programming and safe distributed code generation, with formal guarantees verified in Coq.

Contribution

It introduces a new language for choreographic programming with type safety and deadlock freedom guarantees, verified formally in Coq.

Findings

Ensures message type soundness and deadlock freedom.

Provides a formal verification of the language properties in Coq.

Enables compilation from centralized programs to distributed node programs.

Abstract

We present Pirouette, a 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.