Choreographic programming is an emerging programming paradigm for concurrent and distributed systems, where developers write the communications that should be enacted and a compiler then automatically generates a distributed implementation. Currently, the most advanced incarnation of the paradigm is Choral, an object-oriented choreographic programming language that targets Java. Choral deviated significantly from known theories of choreographies, and in particular introduced the possibility of expressing higher-order choreographies that are fully distributed. In this article, we introduce Chor λ, the first functional choreographic programming language. It is also the first theory that explains the core ideas of higher-order choreographic programming. We show that bridging the gap between practice and theory requires developing a new evaluation strategy and typing discipline for λ terms that accounts for the distributed nature of computation in choreographies.
|Titel||Theoretical Aspects of Computing – ICTAC 2022 - 19th International Colloquium, Proceedings|
|Redaktører||Helmut Seidl, Zhiming Liu, Corina S. Pasareanu|
|Forlag||Springer Science+Business Media|
|Status||Udgivet - 2022|
|Begivenhed||19th International Colloquium on Theoretical Aspects of Computing, ICTAC 2022 - Tbilisi, Georgien|
Varighed: 27. sep. 2022 → 29. sep. 2022
|Konference||19th International Colloquium on Theoretical Aspects of Computing, ICTAC 2022|
|Periode||27/09/2022 → 29/09/2022|
|Navn||Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)|
Bibliografisk noteFunding Information:
Work partially supported by Villum Fonden, grant no. 29518.
© 2022, The Author(s), under exclusive license to Springer Nature Switzerland AG.