By Fabrizio Montesi. Created on: 19 May 2023. 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
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,
s, etc. are process names.
Choreographic languages can be translated to executable distributed code or abstract models of participants by means of endpoint projection.
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
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.
C is essentially a list of instructions (
I), terminated by
Instructions can be read as follows.
p.e -> q.xreads '
eand communicates the resulting value to
q, which stores the value in its local variable
p -> q[L]reads '
pcommunicates the selection label
q'. See knowledge of choice about the role of selections.
p.x := ereads '
eand stores the result in its variable
if p.e then C1 else C2reads 'if
eto the value
true, proceed as
C1, otherwise as
X(p...)means 'the processes
p...stands for a list of process names, e.g.,
p, q, r. Procedures are mapped to choreographies in a context of procedure definitions, and can be recursive.
A choreographic programming language is a choreographic language for expressing executable concurrent and distributed code. See choreographic programming. Recursive Choreographies is a choreographic programming language.
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.
Languages for global types are typically similar to Recursive Choreographies, with some notable key differences:
C1 + C2.
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. , 'Multiparty Asynchronous Session Types', J. ACM 63(1): 9:1-9:67. https://doi.org/10.1145/2827695
Montesi, F. , 'Introduction to Choreographies', Cambridge University Press. https://doi.org/10.1017/9781108981491
Needham, Roger M., Schroeder, Michael D. , 'Using Encryption for Authentication in Large Networks of Computers', Commun. ACM 21(12): 993-999. https://doi.org/10.1145/359657.359659