A Core Model for Choreographic Programming

TL;DR

This paper introduces Core Choreographies (CC), a foundational model for choreographic programming that captures the core primitives, enabling deadlock-free concurrent program synthesis from declarative communication specifications.

Contribution

The paper presents CC as a canonical, minimal model for choreographic programming, capable of implementing any computable function and synthesizing parallel process implementations.

Findings

CC includes only core primitives of choreographic programming.

Any computable function can be implemented in CC.

Process implementations can run computations in parallel.

Abstract

Choreographic Programming is a programming paradigm for building 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.