Alice or Bob?: Process Polymorphism in Choreographies

Eva Graversen, Andrew K. Hirsch, Fabrizio Montesi [2023].
In CoRR abs/2303.04678.

We present PolyChor$\lambda$, a language for higher-order functional \emph{choreographic programming} -- an emerging paradigm by which programmers write the desired cooperative behaviour of a system of communicating processes and then compile it into distributed implementations for each process, a translation called \emph{endpoint projection}. Unlike its predecessor, Chor$\lambda$, PolyChor$\lambda$ has both type and \emph{process} polymorphism inspired by System F$_\omega$. That is, PolyChor$\lambda$ is the first (higher-order) functional choreographic language which gives programmers the ability to write generic choreographies and determine the participants at runtime. This novel combination of features also allows PolyChor$\lambda$ processes to communicate \emph{distributed values}, leading to a new and intuitive way to write delegation. While some of the functional features of PolyChor$\lambda$ give it a weaker correspondence between the semantics of choreographies and their endpoint-projected concurrent systems than some other choreographic languages, we still get the hallmark end result of choreographic programming: projected programs are deadlock-free by design.
Additional notes
Cite (BibTeX)
Click to expand
  author       = {Eva Graversen and
                  Andrew K. Hirsch and
                  Fabrizio Montesi},
  title        = {Alice or Bob?: Process Polymorphism in Choreographies},
  journal      = {CoRR},
  volume       = {abs/2303.04678},
  year         = {2023},
  url          = {},
  doi          = {10.48550/arXiv.2303.04678},
  eprinttype    = {arXiv},
  eprint       = {2303.04678},
  timestamp    = {Wed, 15 Mar 2023 17:23:45 +0100},
  biburl       = {},
  bibsource    = {dblp computer science bibliography,}