Go back to the bliki index

Choreographic Programming

By Fabrizio Montesi. Created on: 19 May 2023. See also: Introduction to Choreographies and Choreographic Programming (Wikipedia)

Choreographic Programming is a programming paradigm where programs are choreographies [Montesi 2013]. A choreographic programming language is a special case of a choreographic language. A program given in a choreographic programming language is called choreographic program, or simply choreography when it is clear from the context.

Alice.modPow(g, a, p) -> Bob.x;
Bob.modPow(g, b, p) -> Alice.y;

A snippet of the Diffie-Hellman protocol for key exchange, given in the language of Recursive Choreographies.

Endpoint Projection (EPP)

Choreographic programming languages are typically accompanied by a compiler, which translates choreographies into executable code for concurrent and distributed systems [Montesi 2023]. The theory of endpoint projection (EPP for short) usually plays an important role in such compilers, in addition to the details of the target executable language. The name 'endpoint projection' was originally introduced by Carbone et al. [2012].

Code for Alice:

send modPow(g, a, p) to Bob;
recv y from Bob;

Code for Bob:

recv x from Alice;
send modPow(g, b, p) to Alice;

Implementations of Alice and Bob compiled from the previous choreography, given in pseudocode.

References

Carbone, M., Honda, K., Yoshida, N. [2012], 'Structured Communication-Centered Programming for Web Services', ACM Trans. Program. Lang. Syst. 34(2): 8:1-8:78. https://doi.org/10.1145/2220365.2220367

Montesi, F. [2013], 'Choreographic Programming', PhD Thesis, IT University of Copenhagen. https://www.fabriziomontesi.com/files/choreographic-programming.pdf

Montesi, F. [2023], 'Introduction to Choreographies', Cambridge University Press. https://doi.org/10.1017/9781108981491