Follow with Edit this page on Go back to the Bliki index

Choreographic Language

By Fabrizio Montesi. Created on 2023-05-17. Last updated on 2023-07-09.
See also: Introduction to Choreographies

A choreographic language is a language for expressing choreographies [Montesi 2023]. Key to choreographic languages is having a high-level primitive for expressing a communication between independent processes (also called roles, or participants). This is inspired by the 'Alice and Bob' notation of security protocols, which presents the primitive

A -> B: M

for expressing the communication of a message M from A (Alice) to B (Bob) [Needham and Schroeder 1978].

Choreographic languages can be roughly divided in two categories:

Another possible source of categorisation: choreographic languages can be textual, graphical, or visual. Some examples are given next. In the remainder, p, q, r, s, etc. are process names.

Choreographic languages can be translated to executable distributed code or abstract models of participants by means of endpoint projection.

Recursive Choreographies

An example of a choreographic language is the language of Recursive Choreographies [Montesi 2023]. I often refer to it examples in the other entries.

Recursive Choreographies is defined by the following grammar, in BNF format (the original presentation is adapted to ASCII here). Note that, in the examples on these pages, I sometimes take the liberty of omitting trailing 0s and else branches.

(Choreographies)	C ::=	I;C							(sequence)
						|	0							(empty choreography)

(Instructions)		I ::=	p.e -> q.x					(value communication)
						|	p -> q[L]					(selection)
						|	p.x := e					(assignment)
						|	if p.e then C1 else C2		(conditional)
						|	X(p...)						(procedure call)

(Expressions)		e ::=	v							(value)
						|	x							(variable)
						|	f(e...)						(function call)

The syntax of Recursive Choreographies [Montesi 2023].

In the syntax, p ranges over process names, L over selection labels (special ), X ranges over procedure names, v ranges over (data) values, x ranges over local variables, and f ranges over function names that are assumed to be defined in a separate language. Each process is assumed to have a local memory store that maps variables to values.

A choreography C is essentially a list of instructions (I), terminated by 0. Instructions can be read as follows.

Choreographic Programming Languages

A choreographic programming language is a choreographic language for expressing executable concurrent and distributed code [Montesi 2013]. See choreographic programming. Recursive Choreographies is a choreographic programming language.

Global Types

Global types are choreographies where communications define propositions about the transmitted data, instead of the computations used to produce or manipulate the data [Honda et al. 2016]. They are often used in theories of static verification for process calculi called multiparty session types [Honda et al. 2016; Hüttel et al. 2016].

Languages for global types are typically similar to Recursive Choreographies, with some notable key differences:

Sequence Diagrams

Sequence diagram are visualisations of choreographies, where the timelines of participants are represented by vertical lines and their interactions by connecting horisontal lines. See sequence diagrams on Wikipedia.

Tools for sequence diagrams typically give a lot of freedom in what can be written about interactions, so the choice of including computation or not can be left to the user.


Honda, K., Yoshida, N., Carbone, M. [2016], 'Multiparty Asynchronous Session Types', J. ACM 63(1): 9:1-9:67.

Hüttel, H., Lanese, I., Vasconcelos, V. T., Caires, L., Carbone, M., Deniélou, P., Mostrous, D., Padovani, L., Ravara, A., Tuosto, E., Vieira, H. T., Zavattaro, G. [2016], 'Foundations of Session Types and Behavioural Contracts', ACM Comput. Surv. 49(1): 3:1-3:36.

Montesi, F. [2013], 'Choreographic Programming', PhD Thesis, IT University of Copenhagen.

Montesi, F. [2023], 'Introduction to Choreographies', Cambridge University Press.

Needham, Roger M., Schroeder, Michael D. [1978], 'Using Encryption for Authentication in Large Networks of Computers', Commun. ACM 21(12): 993-999.