MobilityReadingGroup

Branching Out: Existential External Choice in Effpi

Benjamin ROBINSON , Nobuko YOSHIDA

Effpi [21, 22] 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 [14]. 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 [16].

@inproceedings{RY2026,
  author = {Benjamin Robinson and Nobuko Yoshida},
  title = {{Branching Out: Existential External Choice in Effpi}},
  booktitle = {PLACES 2026},
  pages = {--},
  doi = "https://doi.org/10.4204/EPTCS.444.4",
  year = 2026
}

@inproceedings{RY2026,
  author = {Benjamin Robinson and Nobuko Yoshida},
  title = {{Branching Out: Existential External Choice in Effpi}},
  booktitle = {Proceedings 17th Workshop on Programming Language Approaches to Concurrency and Communication-cEntric Software, 2026, Turing, Italy},
  pages = {--},
  doi = "https://doi.org/10.4204/EPTCS.444.4",
  year = 2026
}