Branching Out: Existential External Choice in Effpi

Journal article

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].

Authors: Robinson, B; Yoshida, N

• Publication status: Published
• Peer review status: Peer reviewed
• Publisher: Open Publishing Association
• Journal: Electronic Proceedings in Theoretical Computer Science
• Volume: 444
• Pages: 34-44
• Publication date: 2026-04-07
• DOI: 10.4204/eptcs.444.4
• ISSN: 2075-2180
• Language: English
• Keywords: Existentialism; Branching (polymer chemistry); Perspective (graphical); Context (archaeology)