A core model for choreographic programming

Choreographic Programming is a paradigm for developing concurrent programs that are deadlock-free by construction, as a result of programming communications declaratively and then synthesising process implementations automatically. Despite strong interest on choreographies, a foundational model that...

Full description

Saved in:
Bibliographic Details
Published in:Theoretical computer science 2020-01, Vol.802, p.38-66
Main Authors: Cruz-Filipe, Luís, Montesi, Fabrizio
Format: Article
Language:English
Subjects:
Choreography
Computability
Process calculi
Citations: Items that this one cites
Items that cite this one
Online Access:Get full text
Tags: Add Tag
No Tags, Be the first to tag this record!
Description
Summary:Choreographic Programming is a paradigm for developing concurrent programs that are deadlock-free by construction, as a result of programming communications declaratively and then synthesising process implementations automatically. Despite strong interest on choreographies, a foundational model that explains which computations can be performed with the hallmark constructs of choreographies is still missing. In this work, we introduce Core Choreographies (CC), a model that includes only the core primitives of choreographic programming. Every computable function can be implemented as a choreography in CC, from which we can synthesise a process implementation where independent computations run in parallel. We discuss the design of CC and argue that it constitutes a canonical model for choreographic programming.
ISSN:0304-3975
1879-2294
DOI:10.1016/j.tcs.2019.07.005