Pirouette: higher-order typed functional choreographies
Keyword(s):
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.
1995 ◽
Vol 5
(1)
◽
pp. 1-35
◽
Keyword(s):
2000 ◽
Vol 10
(02n03)
◽
pp. 239-250
◽
2018 ◽
Vol 2018
◽
pp. 1-6
◽
1992 ◽
Vol 57
(3)
◽
pp. 251-276
◽
1996 ◽
Vol 6
(5)
◽
pp. 409-453
◽
Keyword(s):