Alice or Bob?: Process polymorphism in choreographies

Eva Graversen, Andrew K. Hirsch, Fabrizio Montesi [2024].
In J. Funct. Program. 34.

We present PolyChor $\lambda$ , a language for higher-order functional choreographic programming—an emerging paradigm for concurrent programming. In choreographic programming, programmers write the desired cooperative behaviour of a system of processes and then compile it into an implementation for each process, a translation called endpoint projection. Unlike its predecessor, Chor $\lambda$ , PolyChor $\lambda$ has both type and 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 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 programmes 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      = {J. Funct. Program.},
  volume       = {34},
  year         = {2024},
  url          = {},
  doi          = {10.1017/S0956796823000114},
  timestamp    = {Tue, 07 May 2024 20:27:40 +0200},
  biburl       = {},
  bibsource    = {dblp computer science bibliography,}

A PDF is available (possibly a preprint):

Download PDF