Choreographic programming: Difference between revisions

Revision as of 15:28, 26 June 2023

Revision as of 08:54, 10 September 2023

Line 2:

{{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 }}</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|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 ==

Line 79:

* Chor ([https://www.chor-lang.org/ website]).<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 compiles to [[microservices]] in [[Jolie (programming language)|Jolie]].

* Choral ([https://www.choral-lang.org/ website]). A higher-order, object-oriented choreographic programming language that compiles to libraries in [[Java (programming language)|Java]].

* 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}}</ref> A core theoretical model for choreographic programming. A [[Proof assistant|mechanised]] implementation is available in [[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|s2cid=231802115}}</ref><ref>{{Cite journal |lastlast1=Cruz-Filipe |firstfirst1=Luís |last2=Montesi |first2=Fabrizio |last3=Peressotti |first3=Marco |date=2023-05-27 |title=A Formal Theory of Choreographic Programming |url=https://doi.org/10.1007/s10817-023-09665-3 |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}}</ref><ref>{{Citation |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>

* 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 |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.