# Pirouette: Higher-Order Typed Functional Choreographies

arXiv: https://arxiv.org/abs/2111.03484 · HTML: https://mlsanity.com/paper/2111.03484/

## Key facts

- Cited by 2 papers in the map (data through 14 Oct 2026).
- First posted on arXiv 5 Nov 2021.

## Built on by (most cited first, 2 of 2)

- [Provable Coordination for LLM Agents via Message Sequence Charts](https://mlsanity.com/paper/2604.17612/) (2026)
- [Causal Past Logic for Runtime Verification of Distributed LLM Agent Workflows](https://mlsanity.com/paper/2605.20923/) (2026)

## Abstract (arXiv)

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.