Choreographic Programming is a programming paradigm where programs are choreographies [Montesi 2013]. These programs are written in choreographic programming languages, which feature high-level abstractions for defining the interactions and computations that independent processes engage in. A choreographic programming language is therefore 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.
Choreographic programming languages are typically accompanied by a compiler, which translates choreographies into executable code for concurrent and distributed systems [Montesi 2023]. This code can form standalone applications, libraries, software connectors, etc. Libraries compiled from choreographies can be used in the modular development of distributed applications [Giallorenzo et al. 2020]. The theory of endpoint projection (EPP for short) usually plays an important role in the development of choreography compilers, in addition to the details of the target executable language.
In general a choreography might involve many participants, so EPP must be able to distribute code onto many target programs.
Ideally, EPP should not produce executable code that requires central control (unless this is specified explicitly by the source choreography): choreographies are intended to be decentralised. This introduces an interesting challenge known as knowledge of choice, which deals with ensuring that processes agrees on the alternative behaviours selected during the execution of the choreography.
Theories of EPP are also usually accompanied by proofs that the compiled code is deadlock-free. These proofs leverage the fact that source choreographies do not allow for pairing send and receive actions incorrectly (possibly under the assumption of some well-formedness or well-typedness conditions) [Montesi 2023]. The technique became popular under the slogan of 'deadlock-freedom by design' [Carbone and Montesi 2013].
The term choreographic programming was coined in the titular PhD thesis [Montesi 2013], which proposed the approach as a programming paradigm. The paradigm builds on and extends a series of previous theoretical results on the design of choreographic languages and endpoint projection (e.g., message sequence charts, choreographies for web services, multiparty session types). For historical remarks and an introduction to theory of choreographies and their compilation, see Introduction to Choreographies [Montesi 2023].
There are several mechanisations of choreographic programming in theorem provers.
Carbone, M., Montesi, F. , 'Deadlock-freedom-by-design: multiparty asynchronous global programming', POPL 2013 263-274. https://doi.org/10.1145/2429069.2429101
Cruz-Filipe, L., Lugovic, L., Montesi, F. , 'Certified Compilation of Choreographies with hacc', Proc. FORTE, to appear. arXiv: https://doi.org/10.48550/arXiv.2303.03972
Cruz-Filipe, L., Montesi, F., Peressotti, M. , 'A Formal Theory of Choreographic Programming', J. Autom. Reason. 67(2): 21. https://doi.org/10.1007/s10817-023-09665-3
Dalla Preda, M., Gabbrielli, M., Giallorenzo, S., Lanese, I., Mauro, J. , 'Dynamic Choreographies: Theory And Implementation', Log. Methods Comput. Sci. 13(2). https://doi.org/10.23638/LMCS-13(2:1)2017
Giallorenzo, S., Montesi, F., Peressotti, M. , 'Choral: Object-oriented Choreographic Programming', CoRR abs/2005.09520. https://arxiv.org/abs/2005.09520
Hirsch, A. K., Garg, D. , 'Pirouette: higher-order typed functional choreographies', Proc. ACM Program. Lang. 6(POPL): 1-27. https://doi.org/10.1145/3498684
Montesi, F. , 'Choreographic Programming', PhD Thesis, IT University of Copenhagen. https://www.fabriziomontesi.com/files/choreographic-programming.pdf
Montesi, F. , 'Introduction to Choreographies', Cambridge University Press. https://doi.org/10.1017/9781108981491
Pohjola, J. Å., Gómez-Londoño, A., Shaker, J., Norrish, M. , 'Kalas: A Verified, End-To-End Compiler for a Choreographic Language', Proc. ITP 2022: 27:1-27:18. https://doi.org/10.4230/LIPIcs.ITP.2022.27
Shen, G., Kashiwa, S., Kuper, L. , 'HasChor: Functional Choreographic Programming for All (Functional Pearl)', Proc. ACM Program. Lang. (ICFP), to appear. arXiv: https://doi.org/10.48550/arXiv.2303.00924