Functional Choreographic Programming

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

*Corresponding author for this work

Research output: Chapter in Book/Report/Conference proceedingArticle in proceedingsResearchpeer-review

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.

Original languageEnglish
Title of host publicationTheoretical Aspects of Computing – ICTAC 2022 - 19th International Colloquium, Proceedings
EditorsHelmut Seidl, Zhiming Liu, Corina S. Pasareanu
Number of pages26
PublisherSpringer Science+Business Media
Publication date2022
Pages212-237
ISBN (Print)9783031177149
DOIs
Publication statusPublished - 2022
Event19th International Colloquium on Theoretical Aspects of Computing, ICTAC 2022 - Tbilisi, Georgia
Duration: 27. Sep 202229. Sep 2022

Conference

Conference19th International Colloquium on Theoretical Aspects of Computing, ICTAC 2022
Country/TerritoryGeorgia
CityTbilisi
Period27/09/202229/09/2022
SeriesLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume13572 LNCS
ISSN0302-9743

Keywords

  • Choreographies
  • Concurrency
  • Lambda calculus
  • Type systems

Fingerprint

Dive into the research topics of 'Functional Choreographic Programming'. Together they form a unique fingerprint.

Cite this