Implementing distributed systems is hard. One of the complicated challenges is to "prove"—broadly construed—the absence of communication deadlocks among message-passing processes. A communication deadlock is a form of misbehavior that arises when processes get stuck in cyclic communication dependencies. For instance, Alice might await a message from Bob, while Bob might await a message from Alice. As neither Alice nor Bob sends a message, they are stuck forever.
Choreographic programming (CP) is a method that aims to make implementing distributed systems easier. The benefit of the method is that choreographic programs, called "choreographies", are free of communication deadlocks by construction: if a choreography is well-formed and well-typed at compile-time, then the processes will not get stuck in cyclic communication dependencies at execution-time. For instance, it is impossible in CP to let Alice and Bob await messages from each other without sending any.
The 1CP Language and Tooling (1CPLT) is an extension of Visual Studio Code to apply first-person choreographic programming (1CP) in practice. It is implemented in Rascal. This repository contains:
- examples;
- an LSP server;
- the extension.
- First-Person Choreographic Programming with Continuation-Passing
Communications
Proceedings of ESOP'25 (34th European Symposium on Programming), LNCS 15695, 62-90. 2025.
⭐ EAPLS Best Paper Award
⭐ ETAPS Distinguished Paper Award