Choreographic Quick Changes: First-Class Location (Set) Polymorphism
Fuente:
arXiv
Saved in:
| Main Authors: | , , |
|---|---|
| Format: | Preprint |
| Published: |
2025
|
| Subjects: | |
| Online Access: | |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| _version_ | 1866918128130195456 |
|---|---|
| author | Samuelson, Ashley Hirsch, Andrew K. Cecchetti, Ethan |
| author_facet | Samuelson, Ashley Hirsch, Andrew K. Cecchetti, Ethan |
| contents | Choreographic programming is a promising new paradigm for programming concurrent systems where a developer writes a single centralized program that compiles to individual programs for each node. Existing choreographic languages, however, lack critical features integral to modern systems, like the ability of one node to dynamically compute who should perform a computation and send that decision to others. This work addresses this gap with $λ_{QC}$, the first typed choreographic language with \emph{first class process names} and polymorphism over both types and (sets of) locations. $λ_{QC}$ also improves expressive power over previous work by supporting algebraic and recursive data types as well as multiply-located values. We formalize and mechanically verify our results in Rocq, including the standard choreographic guarantee of deadlock freedom. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2506_10913 |
| institution | arXiv |
| publishDate | 2025 |
| record_format | arxiv |
| spellingShingle | Choreographic Quick Changes: First-Class Location (Set) Polymorphism Samuelson, Ashley Hirsch, Andrew K. Cecchetti, Ethan Programming Languages Choreographic programming is a promising new paradigm for programming concurrent systems where a developer writes a single centralized program that compiles to individual programs for each node. Existing choreographic languages, however, lack critical features integral to modern systems, like the ability of one node to dynamically compute who should perform a computation and send that decision to others. This work addresses this gap with $λ_{QC}$, the first typed choreographic language with \emph{first class process names} and polymorphism over both types and (sets of) locations. $λ_{QC}$ also improves expressive power over previous work by supporting algebraic and recursive data types as well as multiply-located values. We formalize and mechanically verify our results in Rocq, including the standard choreographic guarantee of deadlock freedom. |
| title | Choreographic Quick Changes: First-Class Location (Set) Polymorphism |
| topic | Programming Languages |
| url | https://arxiv.org/abs/2506.10913 |