Choreographic programming: Difference between revisions

Revision as of 03:18, 25 November 2024

Revision as of 18:47, 5 March 2025

Line 75:

== 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 ([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 compilescompiled to [[microservices]] in [[Jolie (programming language)|Jolie]]. In the meantime superseded by Choral.

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

* ChoRus ([https://lsd-ucsc.github.io/ChoRus/ website]). Library-level choreographic programming in [[Rust (programming language)|Rust]].

Line 82:

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

== See also ==