Choreographies as Macros

TL;DR

This paper presents Choret, an embedded choreographic language in Racket, enabling compile-time Endpoint Projection (EPP) to per-participant network programs. It leverages Racket's powerful macros to implement traditional select-and-merge semantics, preserving deadlock freedom while facilitating rapid prototyping. The approach includes a formal network language, a merging mechanism for branching, and compile-time EPP realized entirely as macros. The work demonstrates that a Lisp-family host language can substantially streamline the design and implementation of choreographies, with a compact codebase and practical potential for library-based experimentation.

Abstract

Concurrent programming often entails meticulous pairing of sends and receives between participants to avoid deadlock. Choreographic programming alleviates this burden by specifying the system as a single program. However, there are more applications than implementations of choreographies, and developing new implementations takes a lot of time and effort. Our work uses Racket to expedite building a new choreographic language called Choret. Racket has a powerful macro system which allows Choret to reuse much of its infrastructure for greater functionality and correctness.

Figures (3)

• Figure 1: Choret Syntax
• Figure 2: Network Language Syntax
• Figure 3: Definition of Endpoint Projection (Selected Parts)