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

10 Downloads (Pure)


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
ISBN (Print)9783031177149
Publication statusPublished - 2022
Event19th International Colloquium on Theoretical Aspects of Computing, ICTAC 2022 - Tbilisi, Georgia
Duration: 27. Sept 202229. Sept 2022


Conference19th International Colloquium on Theoretical Aspects of Computing, ICTAC 2022
SeriesLecture Notes in Computer Science
Volume13572 LNCS


  • Choreographies
  • Concurrency
  • Lambda calculus
  • Type systems


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

Cite this