POPL 2022 (series) / POPL Research Papers / Pirouette: Higher-Order Typed Functional Choreographies
Pirouette: Higher-Order Typed Functional ChoreographiesDistinguished PaperInPerson
Fri 21 Jan 2022 10:20 - 10:45 at Salon I - Distributed or Network Programs Chair(s): J. Garrett Morris
We present Pirouette, the first 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.
Fri 21 JanDisplayed time zone: Eastern Time (US & Canada) change
Fri 21 Jan
Displayed time zone: Eastern Time (US & Canada) change
10:20 - 12:00 | |||
10:20 25mResearch paper | Pirouette: Higher-Order Typed Functional ChoreographiesDistinguished PaperInPerson POPL DOI Media Attached | ||
10:45 25mResearch paper | Fair Termination of Binary SessionsRemote POPL DOI Media Attached | ||
11:10 25mResearch paper | Safe, Modular Packet Pipeline ProgrammingRemote POPL DOI Media Attached | ||
11:35 25mResearch paper | Dependently-Typed Data Plane ProgrammingRemote POPL Matthias Eichholz TU Darmstadt, Eric Campbell Cornell University, Matthias Krebs TU Darmstadt, Nate Foster Cornell University, Mira Mezini TU Darmstadt DOI Media Attached |