### Abstract

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 language | English |
---|

Place of Publication | IT University of Copenhagen |
---|---|

ISBN (Print) | 978-87-7949-299-8 |

Publication status | Published - 2013 |

### Fingerprint

### Cite this

*Choreographic Programming*. IT University of Copenhagen.

}

*Choreographic Programming*. IT University of Copenhagen.

**Choreographic Programming.** / Montesi, Fabrizio.

Research output: Book/anthology/thesis/report › Ph.D. thesis › Research

TY - BOOK

T1 - Choreographic Programming

AU - Montesi, Fabrizio

PY - 2013

Y1 - 2013

N2 - Choreographies are descriptions of distributed systems where the developer gives a globalview of how messages are exchanged by endpoint nodes (endpoints for short), instead ofseparately defining the behaviour of each endpoint. They have a significant impact on thequality 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 developmentof programming languages, giving rise to a programming paradigm that in this dissertationwe 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 typicalsafety problems such as deadlocks and race conditions; the concrete implementation ofeach endpoint described in a choreography can then be automatically obtained by compilation, ensuring that such implementations are also safe by construction from the originatingchoreography. However, current formal models for choreographies do not deal with criticalaspects of distributed programming, such as asynchrony, mobility, modularity, and multiparty sessions; it remains thus unclear whether choreographies can still guarantee safetywhen dealing with such nontrivial features.This PhD dissertation argues for the usefulness of choreographic programming as aparadigm for the development of safe distributed systems. We proceed by investigating itsfoundations 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 todistributed implementations in terms of a variant of the π-calculus, the reference model formobile 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 thatLCL 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 inLCL correspond to choreographies; and (ii) the transformations between proofs in LCL toproofs 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 frameworkfor choreographic programming, called Chor. Chor provides an Integrated DevelopmentEnvironment (IDE) for programming with choreographies, equipped with a type checkerfor verifying that choreographies respect protocol specifications given as session types.Programs in Chor can be compiled to executable endpoint implementation in the Jolieprogramming language, a general-purpose language for distributed computing, which weextend to support the development of multiparty asynchronous sessions. We use Chor forevaluating choreographic programming against a series of use cases.

AB - Choreographies are descriptions of distributed systems where the developer gives a globalview of how messages are exchanged by endpoint nodes (endpoints for short), instead ofseparately defining the behaviour of each endpoint. They have a significant impact on thequality 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 developmentof programming languages, giving rise to a programming paradigm that in this dissertationwe 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 typicalsafety problems such as deadlocks and race conditions; the concrete implementation ofeach endpoint described in a choreography can then be automatically obtained by compilation, ensuring that such implementations are also safe by construction from the originatingchoreography. However, current formal models for choreographies do not deal with criticalaspects of distributed programming, such as asynchrony, mobility, modularity, and multiparty sessions; it remains thus unclear whether choreographies can still guarantee safetywhen dealing with such nontrivial features.This PhD dissertation argues for the usefulness of choreographic programming as aparadigm for the development of safe distributed systems. We proceed by investigating itsfoundations 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 todistributed implementations in terms of a variant of the π-calculus, the reference model formobile 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 thatLCL 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 inLCL correspond to choreographies; and (ii) the transformations between proofs in LCL toproofs 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 frameworkfor choreographic programming, called Chor. Chor provides an Integrated DevelopmentEnvironment (IDE) for programming with choreographies, equipped with a type checkerfor verifying that choreographies respect protocol specifications given as session types.Programs in Chor can be compiled to executable endpoint implementation in the Jolieprogramming language, a general-purpose language for distributed computing, which weextend to support the development of multiparty asynchronous sessions. We use Chor forevaluating choreographic programming against a series of use cases.

M3 - Ph.D. thesis

SN - 978-87-7949-299-8

BT - Choreographic Programming

CY - IT University of Copenhagen

ER -