English

Branching Out: Existential External Choice in Effpi

Programming Languages 2026-04-09 v1 Distributed, Parallel, and Cluster Computing

Abstract

Effpi is a framework for writing strongly-typed message-passing programs in Scala, where the compiler enforces the conformance of process implementations to specified protocol types. A compiler plugin is provided to verify properties of protocols, such as deadlock-freedom and liveness, by encoding the behavioural types into a variant of CCS. To address limitations in the expressiveness of the existing toolkit, we extend Effpi with external choice by introducing a branching operation. Upon accepting a message via a branch, protocols enforce a continuation which depends on the label (type) of the received message. We equip the branching operation with the ability to accept messages over more than one channel. Additionally, we introduce a "catch timeout" operation to allow processes to gracefully handle a lack of incoming messages. The enhanced expressiveness of Effpi is demonstrated through a number of examples, including an implementation of the Raft consensus algorithm.

Keywords

Cite

@article{arxiv.2604.06875,
  title  = {Branching Out: Existential External Choice in Effpi},
  author = {Benjamin Robinson and Nobuko Yoshida},
  journal= {arXiv preprint arXiv:2604.06875},
  year   = {2026}
}

Comments

In Proceedings PLACES 2026, arXiv:2604.05737

R2 v1 2026-07-01T11:58:57.435Z