Pirouette: Higher-Order Typed Functional Choreographies

2021/11/05 by Hirsch, Andrew K., Garg, Deepak · 5 citations
#FOS: Computer and information sciences #Programming Languages (cs.PL)

paper · doi:10.48550/arxiv.2111.03484

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.

Cited by

• Choreographic Programming: a Semantic Approach
• Chorex: Restartable, Language-Integrated Choreographies
• Freer Arrows and Why You Need Them in Haskell
• Choreographic Quick Changes: First-Class Location (Set) Polymorphism
• Choreographies as Macros

Related

• Functional Choreographic Programming
• Kickstarting Choreographic Programming
• Choreographies as Macros
• A Formal Theory of Choreographic Programming
• Choreographic Quick Changes: First-Class Location (Set) Polymorphism