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 Jan

Displayed time zone: Eastern Time (US & Canada) change

10:20 - 12:00
Distributed or Network ProgramsPOPL at Salon I
Chair(s): J. Garrett Morris The University of Iowa
10:20
25m
Research paper
Pirouette: Higher-Order Typed Functional ChoreographiesDistinguished PaperInPerson
POPL
Andrew K. Hirsch MPI-SWS, Deepak Garg MPI-SWS
DOI Media Attached
10:45
25m
Research paper
Fair Termination of Binary SessionsRemote
POPL
Luca Ciccone University of Turin, Luca Padovani University of Turin
DOI Media Attached
11:10
25m
Research paper
Safe, Modular Packet Pipeline ProgrammingRemote
POPL
Devon Loehr Princeton University, David Walker Princeton University
DOI Media Attached
11:35
25m
Research 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