Content deleted Content added
Add more languages |
|||
| (13 intermediate revisions by 6 users not shown) | |||
Line 1:
{{short description|Programming paradigm}}
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
== Overview ==
Line 71:
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|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 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]]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://
== Languages ==
* 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 [[Jolie (programming language)|Jolie]].
* Chor
* Choral ([https://www.choral-lang.org/ website]).<ref>{{Cite journal |last1=Giallorenzo |first1=Saverio |last2=Montesi |first2=Fabrizio |last3=Peressotti |first3=Marco |date=2024-01-16 |title=Choral: Object-oriented Choreographic Programming |url=https://dl.acm.org/doi/10.1145/3632398 |journal=ACM Trans. Program. Lang. Syst. |volume=46 |issue=1 |pages=1:1–1:59 |doi=10.1145/3632398 |issn=0164-0925|arxiv=2005.09520 }}</ref><ref>{{cite arXiv |last1=Giallorenzo |first1=Saverio |title=Choral: Object-Oriented Choreographic Programming |date=2023-10-19 |eprint=2005.09520 |last2=Montesi |first2=Fabrizio |last3=Peressotti |first3=Marco|class=cs.PL }}</ref> An object-oriented choreographic programming language that compiles to libraries in [[Java (programming language)|Java]]. Choral is the first choreographic programming language with decentralised data structures and higher-order parameters.
* Choral ([https://www.choral-lang.org/ website]). A higher-order, object-oriented choreographic programming language that compiles to libraries in [[Java (programming language)|Java]].▼
* ChoRus ([https://lsd-ucsc.github.io/ChoRus/ website]). Library-level choreographic programming in [[Rust (programming language)|Rust]].
* 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. A [[Proof assistant|mechanised]] implementation is available in [[Coq (software)|Coq]].<ref>{{Cite book
* HasChor ([https://github.com/gshen42/HasChor website]).<ref>{{Cite journal |
* 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]].
▲*
== See also ==
| |||