Choreographic Programming

Research output: ThesisPh.D. thesis

Abstract

Choreographies are descriptions of distributed systems where the developer gives a global
view of how messages are exchanged by endpoint nodes (endpoints for short), instead of
separately defining the behaviour of each endpoint. They have a significant impact on the
quality of software, as they offer a concise view of the message flows enacted by a system.
For this reason, in the last decade choreographies have been employed in the development
of programming languages, giving rise to a programming paradigm that in this dissertation
we refer to as Choreographic Programming.
Recent formal investigations of choreographies show that they have potential as foundations for the development of safe distributed software. The key idea is that since choreographies abstract from the single input/output actions of endpoints, they avoid typical
safety problems such as deadlocks and race conditions; the concrete implementation of
each endpoint described in a choreography can then be automatically obtained by compilation, ensuring that such implementations are also safe by construction from the originating
choreography. However, current formal models for choreographies do not deal with critical
aspects of distributed programming, such as asynchrony, mobility, modularity, and multiparty sessions; it remains thus unclear whether choreographies can still guarantee safety
when dealing with such nontrivial features.
This PhD dissertation argues for the usefulness of choreographic programming as a
paradigm for the development of safe distributed systems. We proceed by investigating its
foundations and application. To this aim we provide three main contributions.
The first contribution is the development of a formal model and type theory for choreographic programming that support asynchrony, mobility, modular development, and multiparty sessions. We prove that our model guarantees safety by mapping choreographies to
distributed implementations in terms of a variant of the π-calculus, the reference model for
mobile processes. Our translation preserves the expected safety properties of choreographies, among which freedom from deadlocks and race conditions.
The second contribution is the development of Linear Connection Logic (LCL), a formal logic that captures the reasoning behind choreographic programming. We show that
LCL is a conservative extension of Linear Logic. We then develop a Curry-Howard correspondence between LCL and a calculus of choreographies, proving that: (i) proofs in
LCL correspond to choreographies; and (ii) the transformations between proofs in LCL to
proofs in Linear Logic and vice versa correspond to compiling choreography programs to
π-calculus terms and vice versa. The latter result, known as round-trip development, contributes to the open problem of extracting choreographies from existing endpoint programs.
The third contribution is the implementation of a prototype programming framework
for choreographic programming, called Chor. Chor provides an Integrated Development
Environment (IDE) for programming with choreographies, equipped with a type checker
for verifying that choreographies respect protocol specifications given as session types.
Programs in Chor can be compiled to executable endpoint implementation in the Jolie
programming language, a general-purpose language for distributed computing, which we
extend to support the development of multiparty asynchronous sessions. We use Chor for
evaluating choreographic programming against a series of use cases.
Original languageEnglish
Supervisors/Advisors
  • Carbone, Marco, Principal supervisor, External person
Place of PublicationIT University of Copenhagen
Print ISBNs978-87-7949-299-8
Publication statusPublished - 2013

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

Cite this