一句话：提出 Pirouette，一种带类型的高阶函数式编排编程语言，可将中心化程序投影为分布式节点程序，并保证消息类型健全与无死锁。
分布式系统编程通常需分别编写各节点代码，难以保证通信类型安全与全局性质。Pirouette 提供一种带类型的高阶函数式编排编程语言：程序员编写一个中心化的函数式程序，再通过 endpoint projection（端点投影）编译为分布式系统中每个节点的本地程序。该语言在消息的本地语言之上泛型定义，并将其消息类型系统的保证提升到编排层；消息类型健全性同时保证无死锁。所有结果均在 Coq 中机器化验证。
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.
@article{paperbot1571,
title = {Pirouette: higher-order typed functional choreographies},
author = {Andrew K. Hirsch and Deepak Garg},
journal = {Proceedings of the ACM on Programming Languages},
volume = {6},
number = {POPL},
year = {2022},
doi = {10.1145/3498684}
}