Choreographic programming: Difference between revisions

Revision as of 15:11, 11 January 2022

Latest revision as of 13:46, 31 July 2025

(40 intermediate revisions by 17 users not shown)

Line 1:

{{short description|Programming paradigm}}

<!-- {{Programming paradigms}} -->

In [[computer science]], '''choreographic programming''' is a [[programming paradigm]] where programs are compositions of interactions among multiple [[concurrent computing|concurrent]] participants.<ref name="itc">{{cite book |last1=Montesi |first1=Fabrizio |title=Introduction to Choreographies |date=2023 |publisher=Cambridge University Press |doi=10.1017/9781108981491 |isbn=978-1-108-83376-9 |s2cid=102335067 |url=https://doi.org/10.1017/9781108981491}}</ref><ref name="bt-survey">{{Cite journal|url=https://doi.org/10.1561/2500000031|doi = 10.1561/2500000031|title = Behavioral Types in Programming Languages|year = 2016|last1 = Yoshida|first1 = Nobuko|last2 = Vasconcelos|first2 = Vasco T.|last3 = Padovani|first3 = Luca|last4 = Bono|first4 = Nicholas Ng|last5 = Neykova|first5 = Rumyana|last6 = Montesi|first6 = Fabrizio|last7 = Mascardi|first7 = Viviana|last8 = Martins|first8 = Francisco|last9 = Johnsen|first9 = Einar Broch|last10 = Hu|first10 = Raymond|last11 = Giachino|first11 = Elena|last12 = Gesbert|first12 = Nils|last13 = Gay|first13 = Simon J.|last14 = Deniélou|first14 = Pierre-Malo|last15 = Castagna|first15 = Giuseppe|last16 = Campos|first16 = Joana|last17 = Bravetti|first17 = Mario|last18 = Bono|first18 = Viviana|last19 = Ancona|first19 = Davide|journal = Foundations and Trends® in Programming Languages|volume = 3|issue = 2–3|pages = 95–230| hdl=10044/1/44282 |hdl-access = free}}</ref><ref name="mp-langs">{{Cite book|url=https://doi.org/10.4230/LIPIcs.ECOOP.2021.22|doi = 10.4230/LIPIcs.ECOOP.2021.22|year = 2021|last1 = Giallorenzo|first1 = Saverio|last2 = Montesi|first2 = Fabrizio|last3 = Peressotti|first3 = Marco|last4 = Richter|first4 = David|last5 = Salvaneschi|first5 = Guido|last6 = Weisenburger|first6 = Pascal|title = Multiparty Languages: The Choreographic and Multitier Cases (Pearl)|series = Leibniz International Proceedings in Informatics (LIPIcs)|volume = 194|pages = 22:1–22:27| doi-access=free |isbn = 9783959771900}} [https://2021.ecoop.org/details/ecoop-2021-ecoop-research-papers/9/Multiparty-Languages-the-Choreographic-and-Multitier-Cases (ECOOP 2021 Distinguished Paper)]</ref>

== Overview ==

=== Choreographies ===

In choreographic programming, developers use a '''choreographic programming language''' to define the intended communication behaviour of concurrent participants. Programs in this paradigm are called '''choreographies'''.<ref name="bt-surveyitc"/>

Choreographic languages are inspired by [[security protocol notation]] (also known as "Alice and Bob" notation). The key to these languages is the communication primitive, for example

<syntaxhighlight lang="text">

Alice.expr -> Bob.x

</syntaxhighlight>

Line 15:

The example below shows a choreography for a simplified [[single sign-on]] (SSO) protocol based on a [[Central Authentication Service]] (CAS) that involves three roles:

* <code>Client</code>, which wishes to obtain an [[access token]] from <code>CAS</code> to interact with <code>Service</code>.

* <code>Service</code>, which needs to know from <code>CAS</code> if the <code>Client</code> should be given access.

Line 21 ⟶ 20:

The choreography is:

<syntaxhighlight lang="text" line>

1. Client.(credentials, serviceID) -> CAS.authRequest

2. if CAS.check(authRequest) then

3. CAS.token = genToken(authRequest)

4. CAS.Success(token) -> Client.result

5. CAS.Success(token) -> Service.result

6. else

7. CAS.Failure -> Client.result

8. CAS.Failure -> Service.result

</syntaxhighlight>

The choreography starts in Line 1, where <code>Client</code> communicates a pair consisting of some credentials and the identifier of the service it wishes to access to <code>CAS</code>. <code>CAS</code> stores this pair in its local variable <code>authRequest</code> (for authentication request).

In Line 2, the <code>CAS</code> checks if the request is valid for obtaining an authentication token.

If so, it generates a token and communicates a <code>Success</code> message containing the token to both <code>Client</code> and <code>Service</code> (Lines 3—53–5).

Otherwise, the <code>CAS</code> informs <code>Client</code> and <code>Service</code> that authentication failed, by sending a <code>Failure</code> message (Lines 7—87–8). We refer to this choreography as the "SSO choreography" in the remainder.

=== Endpoint Projection ===

A key feature of choreographic programming is the capability of compiling choreographies to distributed implementations. These implementations can be used as libraries infor software that needs to participate in a computer network. by following a protocol,<ref name="itc"/><ref name="mp-langs" /><ref>[https://www.choral-lang.org/ Choral programming language]</ref> or standalone distributed programs.<ref name=":0" /><ref name="aiocj-paper" />

The translation of a choreography into distributed programs is called '''endpoint projection''' (EPP for short).<ref name="bt-survey" /><ref name="mp-langs" />

== Development ==

Endpoint projection returns a program for each role described in the source choreography.<ref name="mp-langs" /> For example, given the choreography above, endpoint projection would return three programs: one for <code>Client</code>, one for <code>Service</code>, and one for <code>CAS</code>. They are shown below in pseudocode form, where <code>send</code> and <code>recv</code> are primitives for sending and receiving messages to/from other roles.

The paradigm of choreographic programming originates from its titular PhD thesis.<ref name="M13:phd">{{cite thesis |type=PhD |last=Montesi |first=Fabrizio |date=2013 |title=Choreographic Programming |url=https://www.fabriziomontesi.com/files/choreographic_programming.pdf |___location= |publisher=IT University of Copenhagen |isbn=978-87-7949-299-8}} [https://eapls.org/items/1855/ (EAPLS Best PhD Dissertation Award)]</ref><ref name="GH21">{{Cite arXiv|eprint=2111.03484|last1=Hirsch|first1=Andrew K.|last2=Garg|first2=Deepak|title=Pirouette: Higher-Order Typed Functional Choreographies|year=2021|class=cs.PL}} [https://popl22.sigplan.org/details/POPL-2022-popl-research-papers/23/Pirouette-Higher-Order-Typed-Functional-Choreographies (POPL 2022 Distinguished Paper)]</ref><ref>{{cite web |url=https://eapls.org/items/1855/ |title=Fabrizio Montesi wins the EAPLS Best PhD Dissertation Award 2014 |author=Arend Rensink |date=2015-08-30 |publisher=European Association for Programming Languages and Systems}}</ref>

{{aligned table|class=wikitable|cols=2|col1header=y|rowstyle=vertical-align:middle

The inspiration for the syntax of choreographic programming languages can be traced back to [[security protocol notation]], also known as "Alice and Bob" notation. Choreographic programming has also been heavily influenced by standards for [[service choreography]] and [[sequence diagram|interaction diagrams]], as well as developments of the theory of [[process calculus|process calculi]].<ref name="mp-langs"/><ref>{{Cite journal|url=https://doi.org/10.1145/2220365.2220367|doi=10.1145/2220365.2220367|title=Structured Communication-Centered Programming for Web Services|year=2012|last1=Carbone|first1=Marco|last2=Honda|first2=Kohei|last3=Yoshida|first3=Nobuko|journal=ACM Transactions on Programming Languages and Systems|volume=34|issue=2|pages=1–78|s2cid=15737118}}</ref>

|title=Endpoint Projection (EPP) of the SSO choreography

|1=Client

|3=Service

|5=CAS

|2=<syntaxhighlight lang="text" line>

send (credentials, serviceID) to CAS

recv result from CAS

</syntaxhighlight>

|4=<syntaxhighlight lang="text" line>

recv result from CAS

</syntaxhighlight>

|6=<syntaxhighlight lang="text" line>

recv authRequest from Client

if check(authRequest) then

token = genToken(authRequest)

send Success(token) to Client

send Success(token) to Service

else

send Failure to Client

send Failure to Service

</syntaxhighlight>

}}

For each role, its code contains the actions that the role should execute to implement the choreography correctly together with the others.

== Development ==

Choreographic programming is an active area of research. The paradigm has been used in the study of [[Information_flow_(information_theory)|information flow]],<ref>{{Cite book|chapter-url=https://doi.org/10.1007/978-3-319-23165-5_20|doi = 10.1007/978-3-319-23165-5_20|chapter = Discretionary Information Flow Control for Interaction-Oriented Specifications|title = Logic, Rewriting, and Concurrency|series = Lecture Notes in Computer Science|year = 2015|last1 = Lluch Lafuente|first1 = Alberto|last2 = Nielson|first2 = Flemming|last3 = Nielson|first3 = Hanne Riis|volume = 9200|pages = 427–450|isbn = 978-3-319-23164-8|url = https://backend.orbit.dtu.dk/ws/files/119987994/Discretionary_Information_Flow_Control_for_Interaction_Oriented_Specifications.pdf}}</ref> [[parallel computing]],<ref>{{Cite book|chapter-url=https://doi.org/10.1007/978-3-319-39570-8_8|doi = 10.1007/978-3-319-39570-8_8|chapter = Choreographies in Practice|title = Formal Techniques for Distributed Objects, Components, and Systems|series = Lecture Notes in Computer Science|year = 2016|last1 = Cruz-Filipe|first1 = Luís|last2 = Montesi|first2 = Fabrizio|volume = 9688|pages = 114–123|arxiv = 1602.08863|isbn = 978-3-319-39569-2|s2cid = 18067252}}</ref> [[cyber-physical system|cyber-physical systems]],<ref>{{Cite book|chapter-url=https://doi.org/10.1145/3019612.3019656|doi=10.1145/3019612.3019656|chapter=Choreographing cyber-physical distributed control systems for the energy sector|title=Proceedings of the Symposium on Applied Computing|year=2017|last1=López|first1=Hugo A.|last2=Heussen|first2=Kai|pages=437–443|isbn=9781450344869|s2cid=39112346}}</ref><ref>{{Cite book|chapter-url=https://doi.org/10.1007/978-3-319-39570-8_13|doi = 10.1007/978-3-319-39570-8_13|chapter = Enforcing Availability in Failure-Aware Communicating Systems|title = Formal Techniques for Distributed Objects, Components, and Systems|series = Lecture Notes in Computer Science|year = 2016|last1 = López|first1 = Hugo A.|last2 = Nielson|first2 = Flemming|last3 = Nielson|first3 = Hanne Riis|volume = 9688|pages = 195–211|isbn = 978-3-319-39569-2}}</ref> [[adaptability|runtime adaptation]],<ref name="aiocj-paper">{{Cite journal|url=https://doi.org/10.23638/LMCS-13(2:1)2017|doi = 10.23638/LMCS-13(2:1)2017|year = 2017|last1 = Preda|first1 = Mila Dalla|last2 = Gabbrielli|first2 = Maurizio|last3 = Giallorenzo|first3 = Saverio|last4 = Lanese|first4 = Ivan|last5 = Mauro|first5 = Jacopo|title = Dynamic Choreographies: Theory and Implementation|journal = Logical Methods in Computer Science ; Volume 13|volume = 13|issue = 2|s2cid = 5555662}}</ref> and [[system integration]].<ref>{{Cite book|chapter-url=https://doi.org/10.1007/978-3-030-02671-4_2|doi = 10.1007/978-3-030-02671-4_2|chapter = ChIP: A Choreographic Integration Process|title = On the Move to Meaningful Internet Systems. OTM 2018 Conferences|series = Lecture Notes in Computer Science|year = 2018|last1 = Giallorenzo|first1 = Saverio|last2 = Lanese|first2 = Ivan|last3 = Russo|first3 = Daniel|volume = 11230|pages = 22–40|isbn = 978-3-030-02670-7|url = https://findresearcher.sdu.dk:8443/ws/files/153104697/ChIP.pdf}}</ref>

The paradigm of choreographic programming originates from its titular PhD thesis.<ref name="M13:phd">{{cite thesis |type=PhD |last=Montesi |first=Fabrizio |date=2013 |title=Choreographic Programming |url=https://www.fabriziomontesi.com/files/choreographic_programming.pdf |___location= |publisher=IT University of Copenhagen |isbn=978-87-7949-299-8}} [https://eapls.org/items/1855/ (EAPLS Best PhD Dissertation Award)]</ref><ref name="GH21">{{Citecite journal arXiv|eprint=2111.03484|last1=Hirsch |first1=Andrew K. |last2=Garg |first2=Deepak |title=Pirouette: Higherhigher-Orderorder Typedtyped Functionalfunctional choreographies Choreographies|yearjournal=2021Proceedings of the ACM on Programming Languages |classdate=cs16 January 2022 |volume=6 |issue=POPL |pages=1–27 |doi=10.PL1145/3498684|s2cid=243833095 |doi-access=free |arxiv=2111.03484 }} [https://popl22.sigplan.org/details/POPL-2022-popl-research-papers/23/Pirouette-Higher-Order-Typed-Functional-Choreographies (POPL 2022 Distinguished Paper)]</ref><ref>{{cite web |url=https://eapls.org/items/1855/ |title=Fabrizio Montesi wins the EAPLS Best PhD Dissertation Award 2014 |author=Arend Rensink |date=2015-08-30 |publisher=European Association for Programming Languages and Systems}}</ref>

The inspiration for the syntax of choreographic programming languages can be traced back to [[security protocol notation]], also known as "Alice and Bob" notation.<ref name="itc"/> Choreographic programming has also been heavily influenced by standards for [[service choreography]] and [[sequence diagram|interaction diagrams]], as well as developments of the theory of [[process calculus|process calculi]].<ref name="itc"/><ref name="mp-langs"/><ref>{{Cite journal|url=https://doi.org/10.1145/2220365.2220367|doi=10.1145/2220365.2220367|title=Structured Communication-Centered Programming for Web Services|year=2012|last1=Carbone|first1=Marco|last2=Honda|first2=Kohei|last3=Yoshida|first3=Nobuko|journal=ACM Transactions on Programming Languages and Systems|volume=34|issue=2|pages=1–78|s2cid=15737118|doi-access=free}}</ref>

Choreographic programming is an active area of research. The paradigm has been used in the study of [[Information_flow_Information flow (information_theoryinformation theory)|information flow]],<ref>{{Cite book|chapter-url=https://doi.org/10.1007/978-3-319-23165-5_20|doi = 10.1007/978-3-319-23165-5_20|chapter = Discretionary Information Flow Control for Interaction-Oriented Specifications|title = Logic, Rewriting, and Concurrency|series = Lecture Notes in Computer Science|year = 2015|last1 = Lluch Lafuente|first1 = Alberto|last2 = Nielson|first2 = Flemming|last3 = Nielson|first3 = Hanne Riis|author3-link=Hanne Riis Nielson|volume = 9200|pages = 427–450|isbn = 978-3-319-23164-8| s2cid=32617923 |url = https://backend.orbit.dtu.dk/ws/files/119987994/Discretionary_Information_Flow_Control_for_Interaction_Oriented_Specifications.pdf}}</ref> [[parallel computing]],<ref>{{Cite book|chapter-url=https://doi.org/10.1007/978-3-319-39570-8_8|doi = 10.1007/978-3-319-39570-8_8|chapter = Choreographies in Practice|title = Formal Techniques for Distributed Objects, Components, and Systems|series = Lecture Notes in Computer Science|year = 2016|last1 = Cruz-Filipe|first1 = Luís|last2 = Montesi|first2 = Fabrizio|volume = 9688|pages = 114–123|arxiv = 1602.08863|isbn = 978-3-319-39569-2|s2cid = 18067252}}</ref> [[cyber-physical system|cyber-physical systems]]s,<ref>{{Cite book|chapter-url=https://doi.org/10.1145/3019612.3019656|doi=10.1145/3019612.3019656|chapter=Choreographing cyber-physical distributed control systems for the energy sector|title=Proceedings of the Symposium on Applied Computing|year=2017|last1=López|first1=Hugo A.|last2=Heussen|first2=Kai|pages=437–443|isbn=9781450344869|s2cid=39112346}}</ref><ref>{{Cite book|chapter-url=https://doiinria.org/10hal.1007science/978hal-3-319-39570-8_1301432918|doi = 10.1007/978-3-319-39570-8_13|chapter = Enforcing Availability in Failure-Aware Communicating Systems|title = Formal Techniques for Distributed Objects, Components, and Systems|series = Lecture Notes in Computer Science|year = 2016|last1 = López|first1 = Hugo A.|last2 = Nielson|first2 = Flemming|last3 = Nielson|first3 = Hanne Riis|author3-link=Hanne Riis Nielson|volume = 9688|pages = 195–211|isbn = 978-3-319-39569-2| s2cid=12872876 }}</ref> [[adaptability|runtime adaptation]],<ref name="aiocj-paper">{{Cite journal|url=https://doi.org/10.23638/LMCS-13(2:1)2017|doi = 10.23638/LMCS-13(2:1)2017|year = 2017|last1 = Preda|first1 = Mila Dalla|last2 = Gabbrielli|first2 = Maurizio|last3 = Giallorenzo|first3 = Saverio|last4 = Lanese|first4 = Ivan|last5 = Mauro|first5 = Jacopo|title = Dynamic Choreographies: Theory and Implementation|journal = Logical Methods in Computer Science ; Volume 13|volume = 13|issue = 2|s2cid = 5555662|arxiv = 1611.09067}}</ref> and [[system integration]].<ref>{{Cite book|chapter-url=https://doi.org/10.1007/978-3-030-02671-4_2|doi = 10.1007/978-3-030-02671-4_2|chapter = ChIP: A Choreographic Integration Process|title = On the Move to Meaningful Internet Systems. OTM 2018 Conferences|series = Lecture Notes in Computer Science|year = 2018|last1 = Giallorenzo|first1 = Saverio|last2 = Lanese|first2 = Ivan|last3 = Russo|first3 = Daniel|volume = 11230|pages = 22–40|isbn = 978-3-030-02670-7| s2cid=53015580 |url = https://findresearcher.sdu.dk:8443/ws/files/153104697/ChIP.pdf}}</ref>

== Languages ==

* AIOCJ ([http://www.cs.unibo.it/projects/jolie/aiocj.html website]).<ref name="aiocj-paper"/> A choreographic programming language for [[Adaptation_Adaptation (computer_sciencecomputer science)|adaptable systems]] that produces code in in [[Jolie (programming language)|Jolie]].

* Chor.<ref name=":0">{{Cite book|chapter-url=https://doi.org/10.1145/2429069.2429101|doi=10.1145/2429069.2429101|chapter=Deadlock-freedom-by-design|title=Proceedings of the 40th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages - POPL '13|year=2013|last1=Carbone|first1=Marco|last2=Montesi|first2=Fabrizio|page=263|isbn=9781450318327|s2cid=15627190}}</ref> A [[session type|session-typed]] choreographic programming language that compiled to [[microservices]] in [[Jolie (programming language)|Jolie]]. In the meantime superseded by Choral.

* AIOCJ ([http://www.cs.unibo.it/projects/jolie/aiocj.html website]).<ref name="aiocj-paper"/> A choreographic programming language for [[Adaptation_(computer_science)|adaptable systems]] that produces code in in [[Jolie (programming language)|Jolie]].

* ChorChoral ([https://www.chorchoral-lang.org/ website]).<ref>{{Cite bookjournal |chapterlast1=Giallorenzo |first1=Saverio |last2=Montesi |first2=Fabrizio |last3=Peressotti |first3=Marco |date=2024-01-16 |title=Choral: Object-oriented Choreographic Programming |url=https://doidl.acm.org/doi/10.1145/24290693632398 |journal=ACM Trans.2429101 Program. Lang. Syst. |volume=46 |issue=1 |pages=1:1–1:59 |doi=10.1145/2429069.24291013632398 |chapterissn=Deadlock-freedom-by0164-design0925|titlearxiv=Proceedings2005.09520 of}}</ref><ref>{{cite thearXiv 40th|last1=Giallorenzo annual|first1=Saverio ACM|title=Choral: SIGPLANObject-SIGACT symposiumOriented onChoreographic Principles of programming languagesProgramming |date=2023-10-19 POPL '13|yeareprint=2013|last1=Carbone|first1=Marco2005.09520 |last2=Montesi |first2=Fabrizio |pagelast3=263Peressotti |isbnfirst3=9781450318327Marco|s2cidclass=15627190cs.PL }}</ref> AAn [[session type|sessionobject-typed]]oriented choreographic programming language that compiles to [[microservices]]libraries in [[JolieJava (programming language)|JolieJava]]. Choral is the first choreographic programming language with decentralised data structures and higher-order parameters.

* ChoralChoRus ([https://www.chorallsd-langucsc.orggithub.io/ChoRus/ website]). A higherLibrary-order, object-orientedlevel choreographic programming language that compiles to libraries in [[JavaRust (programming language)|JavaRust]].

* Core Choreographies.<ref>{{Cite journal|url=https://doi.org/10.1016/j.tcs.2019.07.005|doi = 10.1016/j.tcs.2019.07.005|title = A core model for choreographic programming|year = 2020|last1 = Cruz-Filipe|first1 = Luís|last2 = Montesi|first2 = Fabrizio|journal = Theoretical Computer Science|volume = 802|pages = 38–66|s2cid = 199122777|arxiv = 1510.03271}}</ref> A core theoretical model for choreographic programming. AnA [[Proof assistant|mechanised]] implementation is available in [[Coq (software)|Coq]].<ref>{{Cite book|url=https://doi.org/10.4230/LIPIcs.ITP.2021.15|doi=10.4230/LIPIcs.ITP.2021.15|isbn=9783959771887|title=Formalising a Turing-Complete Choreographic Language in Coq|series=Leibniz International Proceedings in Informatics (LIPIcs)|year=2021|volume=193|pages=15:1–15:18|last1=Cohen|first1=Liron|last2=Kaliszyk|first2=Cezary|doi-access=free |s2cid=231802115}}</ref><ref>{{Cite journal |last1=Cruz-Filipe |first1=Luís |last2=Montesi |first2=Fabrizio |last3=Peressotti |first3=Marco |date=2023-05-27 |title=A Formal Theory of Choreographic Programming |journal=Journal of Automated Reasoning |language=en |volume=67 |issue=2 |pages=21 |doi=10.1007/s10817-023-09665-3 |s2cid=252090305 |issn=1573-0670|doi-access=free |arxiv=2209.01886 }}</ref><ref>{{cite book |last1=Cruz-Filipe |first1=Luís |title=Certifying Choreography Compilation |date=2021 |url=https://link.springer.com/10.1007/978-3-030-85315-0_8 |work=Theoretical Aspects of Computing – ICTAC 2021 |volume=12819 |pages=115–133 |editor-last=Cerone |editor-first=Antonio |place=Cham |publisher=Springer International Publishing |language=en |doi=10.1007/978-3-030-85315-0_8 |isbn=978-3-030-85314-3 |access-date=2022-03-07 |last2=Montesi |first2=Fabrizio |last3=Peressotti |first3=Marco |series=Lecture Notes in Computer Science |arxiv=2102.10698 |s2cid=231985665 |editor2-last=Ölveczky |editor2-first=Peter Csaba}}</ref>

* HasChor ([https://github.com/gshen42/HasChor website]).<ref>{{Cite journal |last1=Shen |first1=Gan |last2=Kashiwa |first2=Shun |last3=Kuper |first3=Lindsey |title=HasChor: Functional Choreographic Programming for All (Functional Pearl) |journal=Proceedings of the ACM on Programming Languages |date=2023-08-31 |volume=7 |url=https://doi.org/10.1145/3607849 |pages= 541–565|doi=10.1145/3607849|arxiv=2303.00924 }}</ref> A library for choreographic programming in [[Haskell]].

* Kalas.<ref>{{Cite journal |last1=Pohjola |first1=Johannes Åman |last2=Gómez-Londoño |first2=Alejandro |last3=Shaker |first3=James |last4=Norrish |first4=Michael |date=2022 |editor-last=Andronick |editor-first=June |editor2-last=de Moura |editor2-first=Leonardo |title=Kalas: A Verified, End-To-End Compiler for a Choreographic Language |url=https://drops.dagstuhl.de/opus/volltexte/2022/16736 |journal=13th International Conference on Interactive Theorem Proving (ITP 2022) |series=Leibniz International Proceedings in Informatics (LIPIcs) |___location=Dagstuhl, Germany |publisher=Schloss Dagstuhl – Leibniz-Zentrum für Informatik |volume=237 |pages=27:1–27:18 |doi=10.4230/LIPIcs.ITP.2022.27 |doi-access=free |isbn=978-3-95977-252-5|s2cid=251322644 }}</ref> A choreographic programming language with a verified compiler to CakeML.

* Pirouette.<ref name="GH21"/> A [[proof assistant|mechanised]] choreographic programming language theory with higher-order procedures.

* Klor ([https://github.com/lovrosdu/klor website]). Library-level choreographic programming in [[Clojure]].

* Tempo ([https://github.com/tempo-lang/tempo website]). A practical choreographic programming language that compiles to library source code for multiple target languages.

== See also ==

Line 59 ⟶ 89:

* [[Sequence diagram]]

* [[Service choreography]]

* [[Structured concurrency]]

* [[Multitier programming]]

== References ==

<!--- See http://en.wikipedia.org/wiki/Wikipedia:Footnotes on how to create references using <ref></ref> tags, these references will then appear here automatically -->

{{Reflist}}

== External links ==

* [https://www.choral-lang.org/ www.choral-lang.org]

<!-- {{Programming paradigms navbox}} -->

* [https://www.choral-lang.org www.choral-lang.org]

<!--- Categories --->

[[:Category:Concurrent computing]]

[[:Category:Programming paradigms]]