Pirouette: Higher-Order Typed Functional Choreographies
英文摘要：
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.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
