CP 2024
as the organisers put it
Choreographies are coordination plans for concurrent and distributed systems. A choreography defines the roles of the involved participants and how they are supposed to work together. In the emerging paradigm of choreographic programming (CP), choreographies are programs that can be compiled to executable implementations. CP originated primarily in the context of process calculi, with preliminary work done to establish its foundations and experiment with implementations. Recently, several proposals have shown that one can adapt CP to work in synergy with mainstream programming paradigms, ...
who it's for
programming language designers, distributed systems engineers, formal methods engineers, rust developers, clojure developers, tool and library authors, systems architects
topics
algebraic effects for choreographies; endpoint projection via effect handlers; embedded Rust DSLs for distribution; staged per-location code generation; multicast and multiply located values; modal type theory for choreography; probabilistic choreographies to PRISM; placement algebra and placed types; communication failure models and recovery; amendment transformation for unrealizable choreographies
| title | author | length |
|---|---|---|
| Toward Verified Library-Level Choreographic Programming with Algebraic Effects | Gan Shen, Lindsey Kuper | 22m |
Claims that algebraic effects give a lightweight, formalizable basis for library-level choreographies, and presents an Agda prototype that models choreography… | ||
| Suki: Choreographed Distributed Dataflow in Rust | Shadaj Laddad, Alvin Cheung, Joseph M. Hellerstein | 19m |
Suki is an embedded Rust DSL that uses staged programming to emit per-location Rust sources which compile to zero‑overhead binaries, relying on the hydroflow… | ||
| Klor: Choreographies for the Working Clojurian | Lovro Lugović, Sung-Shik Jongmans | 21m |
Klor is a Clojure EDSL for choreographies developed in about six to seven months that performs compile-time projection via a defchor macro which expands into… | ||
| ChoRus: Library-Level Choreographic Programming in Rust | Shun Kashiwa, Lindsey Kuper | 21m |
ChoRus is a Rust cargo library that implements choreographic programming by compiling a global choreography to node code using endpoint projection via… | ||
| We Know I Know You Know; Choreographic Programming With Multicast and Multiply Located Values | Mako P. Bates, Joseph P. Near | 19m |
A new choreographic language 𐤄λsmall adds multiply located values and multicast so a value can be located at many parties; typechecking now implies deadlock… | ||
| Exploring Algebraic Placement in Multiparty Languages | George Zakhour, Pascal Weisenburger, Guido Salvaneschi | 19m |
Claims that placement systems mirror type-system structure and that a type-checker can be repurposed into a placement checker, demonstrated by a Scala… | ||
| A Probabilistic Choreography Language for PRISM | Marco Carbone, Adele Veschetti | 19m |
A choreographic specification language gives global descriptions of concurrent probabilistic interactions, defines a probabilistic semantics, and provides a… | ||
| Corps: A Core Calculus of Hierarchical Choreographic Programming | Andrew K. Hirsch | 36m |
Claims that choreographic located types correspond to doxastic modalities and that adding explicit trust yields authorization logic as the right… | ||
| Choreographies meet Communication Failures | Eva Graversen, Fabrizio Montesi, Marco Peressotti | 21m |
A choreography language models three concrete failure modes — send omission, receive omission, and emission failure — by declaring paired frames K/K' with… | ||
| Choreographic Programming in Modal Type Theory | Maxim Urschumzew, MiĊętek Bak | 21m |
An instantiation of Modal Type Theory (MTT) maps Chorλ location annotations to modalities, adds two primitives—prepare (schedule a local value into a… | ||
| A Propositional Dynamic Logic for Choreographies | Matteo Acclavio, Fabrizio Montesi, Marco Peressotti | 23m |
Generalises propositional dynamic logic into operational propositional dynamic logic (OPDL) that separates trace reasoning from operational semantics… | ||
| Choreographic Programming: its essence, beauty, and necessity | Fabrizio Montesi | 01h 02m |
Claims a communication-first programming model where a choreography compiles to correct per-participant code, yielding deadlock freedom by construction… | ||
| nothing matches | ||