Functional choreographic programming

DOI10.1007/978-3-031-17715-6_15MaRDI QIDQ6109477zbMATH OpenFDO

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

Publication date 28 July 2023

Published in Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL https://arxiv.org/abs/2111.03701

zbMATH Keywords

choreographiesconcurrencylambda calculustype systems

Mathematics Subject Classification ID

Theory of computing (68Qxx)

Abstract: Choreographic programming is an emerging programming paradigm for concurrent and distributed systems, whereby developers write the communications that should be enacted and then a distributed implementation is automatically obtained by means of a compiler. Theories of choreographic programming typically come with strong theoretical guarantees about the compilation process, most notably: the generated implementations operationally correspond to their source choreographies and are deadlock-free. 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 introduced the possibility of expressing higher-order choreographies (choreographies parameterised over choreographies) that are fully distributed. As a consequence, it is unclear if the usual guarantees of choreographies can still hold in the more general setting of higher-order ones. We introduce Chor{lambda}, the first functional choreographic programming language: it introduces a new formulation of the standard communication primitive found in choreographies as a function, and it is based upon the {lambda}-calculus. Chor{lambda} is the first theory that explains the core ideas of higher-order choreographic programming (as in Choral). Bridging the gap between practice and theory requires developing a new evaluation strategy and typing discipline for {lambda} terms that accounts for the distributed nature of computation in choreographies. We illustrate the expressivity of Chor{lambda} with a series of examples, which include reconstructions of the key examples from the original presentation of Choral. Our theory supports the expected properties of choreographic programming and bridges the gap between the communities of functional and choreographic programming.

Cites work

• scientific article; zbMATH DE number 6703933 (Why is no real title available?)
• scientific article; zbMATH DE number 7699432 (Why is no real title available?)
• A core model for choreographic programming
• A predicate transformer for choreographies. Computing preconditions in choreographic programming
• Binary session types for psi-calculi
• Certifying choreography compilation
• Deadlock-freedom-by-design, multiparty asynchronous global programming
• Enforcing availability in failure-aware communicating systems
• Functional choreographic programming
• Mobile ambients
• Multiparty asynchronous session types
• Nested protocols in session types
• New directions in cryptography
• Procedural Choreographic Programming
• Structured Communication-Centred Programming for Web Services
• Types and programing languages
• Using encryption for authentication in large networks of computers

Cited in

(4)

• Procedural Choreographic Programming
• Functional choreographic programming
• A core model for choreographic programming
• Developing software for dancing tango in Compás

This page was built for publication: Functional choreographic programming

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q6109477)