Functional Choreographic Programming

Luís Cruz-Filipe; Eva Graversen; Lovro Lugović; Fabrizio Montesi; Marco Peressotti

doi:10.1007/978-3-031-17715-6_15

Functional Choreographic Programming

Luís Cruz-Filipe, Eva Graversen^*, Lovro Lugović, Fabrizio Montesi, Marco Peressotti

^*Kontaktforfatter

Syddansk Universitet

Publikation: Kapitel i bog/rapport/konference-proceeding › Konferencebidrag i proceedings › Forskning › peer review

Abstrakt

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.

Originalsprog	Engelsk
Titel	Theoretical Aspects of Computing – ICTAC 2022 - 19th International Colloquium, Proceedings
Redaktører	Helmut Seidl, Zhiming Liu, Corina S. Pasareanu
Antal sider	26
Forlag	Springer Science+Business Media
Publikationsdato	2022
Sider	212-237
ISBN (Trykt)	9783031177149
DOI	https://doi.org/10.1007/978-3-031-17715-6_15
Status	Udgivet - 2022
Begivenhed	19th International Colloquium on Theoretical Aspects of Computing, ICTAC 2022 - Tbilisi, Georgien Varighed: 27. sep. 2022 → 29. sep. 2022

Konference

Konference	19th International Colloquium on Theoretical Aspects of Computing, ICTAC 2022
Land/Område	Georgien
By	Tbilisi
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)
Vol/bind	13572 LNCS
ISSN	0302-9743

Bibliografisk note

Funding Information:
Work partially supported by Villum Fonden, grant no. 29518.

Publisher Copyright:
© 2022, The Author(s), under exclusive license to Springer Nature Switzerland AG.

Dokumenter og links

10.1007/978-3-031-17715-6_15

Dokument under embargo

Open access version
Accepteret manuskript, 623 KB
Licens: CC BY-NC-ND
Embargo slutter: 03/10/2023

Citationsformater

Cruz-Filipe, L., Graversen, E., Lugović, L., Montesi, F., & Peressotti, M. (2022). Functional Choreographic Programming. I H. Seidl, Z. Liu, & C. S. Pasareanu (red.), Theoretical Aspects of Computing – ICTAC 2022 - 19th International Colloquium, Proceedings (s. 212-237). Springer Science+Business Media. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) Bind 13572 LNCS https://doi.org/10.1007/978-3-031-17715-6_15

Cruz-Filipe, Luís ; Graversen, Eva ; Lugović, Lovro et al. / Functional Choreographic Programming. Theoretical Aspects of Computing – ICTAC 2022 - 19th International Colloquium, Proceedings. red. / Helmut Seidl ; Zhiming Liu ; Corina S. Pasareanu. Springer Science+Business Media, 2022. s. 212-237 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), Bind 13572 LNCS).

@inproceedings{732e820db3174aa494a46def8469de95,

title = "Functional Choreographic Programming",

abstract = "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.",

keywords = "Choreographies, Concurrency, Lambda calculus, Type systems",

author = "Lu{\'i}s Cruz-Filipe and Eva Graversen and Lovro Lugovi{\'c} and Fabrizio Montesi and Marco Peressotti",

note = "Funding Information: Work partially supported by Villum Fonden, grant no. 29518. Publisher Copyright: {\textcopyright} 2022, The Author(s), under exclusive license to Springer Nature Switzerland AG.; 19th International Colloquium on Theoretical Aspects of Computing, ICTAC 2022 ; Conference date: 27-09-2022 Through 29-09-2022",

year = "2022",

doi = "10.1007/978-3-031-17715-6_15",

language = "English",

isbn = "9783031177149",

series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",

publisher = "Springer Science+Business Media",

pages = "212--237",

editor = "Helmut Seidl and Zhiming Liu and Pasareanu, {Corina S.}",

booktitle = "Theoretical Aspects of Computing – ICTAC 2022 - 19th International Colloquium, Proceedings",

address = "United States",

}

Cruz-Filipe, L , Graversen, E, Lugović, L, Montesi, F & Peressotti, M 2022, Functional Choreographic Programming. i H Seidl, Z Liu & CS Pasareanu (red), Theoretical Aspects of Computing – ICTAC 2022 - 19th International Colloquium, Proceedings. Springer Science+Business Media, Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), bind 13572 LNCS, s. 212-237, 19th International Colloquium on Theoretical Aspects of Computing, ICTAC 2022, Tbilisi, Georgien, 27/09/2022. https://doi.org/10.1007/978-3-031-17715-6_15

Functional Choreographic Programming. / Cruz-Filipe, Luís ; Graversen, Eva; Lugović, Lovro et al.

Theoretical Aspects of Computing – ICTAC 2022 - 19th International Colloquium, Proceedings. red. / Helmut Seidl; Zhiming Liu; Corina S. Pasareanu. Springer Science+Business Media, 2022. s. 212-237 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), Bind 13572 LNCS).

Publikation: Kapitel i bog/rapport/konference-proceeding › Konferencebidrag i proceedings › Forskning › peer review

TY - GEN

T1 - Functional Choreographic Programming

AU - Cruz-Filipe, Luís

AU - Graversen, Eva

AU - Lugović, Lovro

AU - Montesi, Fabrizio

AU - Peressotti, Marco

PY - 2022

Y1 - 2022

N2 - 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.

AB - 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.

KW - Choreographies

KW - Concurrency

KW - Lambda calculus

KW - Type systems

U2 - 10.1007/978-3-031-17715-6_15

DO - 10.1007/978-3-031-17715-6_15

M3 - Article in proceedings

AN - SCOPUS:85140755772

SN - 9783031177149

T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

SP - 212

EP - 237

BT - Theoretical Aspects of Computing – ICTAC 2022 - 19th International Colloquium, Proceedings

A2 - Seidl, Helmut

A2 - Liu, Zhiming

A2 - Pasareanu, Corina S.

PB - Springer Science+Business Media

T2 - 19th International Colloquium on Theoretical Aspects of Computing, ICTAC 2022

Y2 - 27 September 2022 through 29 September 2022

ER -

Cruz-Filipe L , Graversen E, Lugović L, Montesi F , Peressotti M. Functional Choreographic Programming. I Seidl H, Liu Z, Pasareanu CS, red., Theoretical Aspects of Computing – ICTAC 2022 - 19th International Colloquium, Proceedings. Springer Science+Business Media. 2022. s. 212-237. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), Bind 13572 LNCS). doi: 10.1007/978-3-031-17715-6_15

Functional Choreographic Programming

Abstrakt

Konference

Bibliografisk note

Dokumenter og links

Dokument under embargo

Fingeraftryk

Citationsformater