Alice or Bob?: Process polymorphism in choreographies

DOI10.1017/S0956796823000114MaRDI QIDQ6131906zbMATH OpenWikidataFDO

Authors Eva Graversen, Fabrizio Montesi

Publication date 18 April 2024

Published in Journal of Functional Programming (Search for Journal in Brave)

Copyright license Creative Commons Attribution 4.0 International

Full work available at URL https://arxiv.org/abs/2303.04678

Mathematics Subject Classification ID

Functional programming and lambda calculus (68N18)

Abstract: 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${}_{o}mega$. 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.

This page was built for publication: Alice or Bob?: Process polymorphism in choreographies

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q6131906)