pith. sign in

arxiv: 2604.06875 · v1 · submitted 2026-04-08 · 💻 cs.PL · cs.DC

Branching Out: Existential External Choice in Effpi

Benjamin Robinson (University of Oxford) , Nobuko Yoshida (University of Oxford) This is my paper

Pith reviewed 2026-05-10 18:14 UTC · model grok-4.3

classification 💻 cs.PL cs.DC
keywords EffpiScalasession typesexternal choicebranchingmessage passingRaft consensusdeadlock freedom
0
0 comments X

The pith

Effpi gains a branching operation for external choice that picks label-dependent continuations across multiple channels, plus catch-timeout handling.

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The paper extends the Effpi framework for strongly-typed message-passing programs in Scala. It adds a branching construct that lets a protocol accept a message and then continue according to the label or type of that message, with the option to listen on more than one channel at once. A catch-timeout operation is also added so processes can respond when no message arrives. These features are designed to preserve the existing compiler plugin's ability to verify deadlock-freedom and liveness by encoding the extended protocols into a variant of CCS. The authors illustrate the gain in expressiveness with several examples, one of which is a complete implementation of the Raft consensus algorithm.

Core claim

We introduce a branching operation to Effpi that realises existential external choice: upon receiving a message the protocol is forced into a continuation determined by the label of the received message, and the operation can accept over several channels simultaneously. We further equip the language with a catch-timeout construct that allows processes to handle the absence of incoming messages gracefully. Both additions are shown to be encodable into the CCS model already used by the verification plugin, so that deadlock-freedom and liveness properties continue to be checked automatically. The enhanced language is exercised on a collection of examples that include an implementation of the RA

What carries the argument

The branching operation, which accepts a labelled message on one or more channels and enforces a continuation that depends on the received label.

If this is right

  • Protocols that require external choice can now be written and verified inside Effpi.
  • Multi-channel branching enables a single process to react to messages arriving on any of several channels.
  • Catch-timeout lets typed processes handle communication failure without leaving the protocol.
  • Consensus algorithms such as Raft can be expressed and checked for liveness inside the framework.

Where Pith is reading between the lines

These are editorial extensions of the paper, not claims the author makes directly.

  • The same encoding technique might be reusable for other session-type extensions that currently lack a CCS model.
  • Larger distributed systems built on Effpi could now incorporate leader-election or replication logic directly.
  • The multi-channel branch may generalise to choice over channels with different payload types.

Load-bearing premise

The new branching and catch-timeout constructs can be encoded into the CCS variant used by the compiler plugin without losing soundness or completeness of the deadlock-freedom and liveness checks.

What would settle it

A concrete protocol written with the new branching operation for which the CCS-based verifier either reports a deadlock that does not exist or fails to report a deadlock that does exist.

Figures

Figures reproduced from arXiv: 2604.06875 by Benjamin Robinson (University of Oxford), Nobuko Yoshida (University of Oxford).

Figure 1
Figure 1. Figure 1: A faulty implementation of the AuctionHouse protocol by merging two channels. With these motivating examples, we have identified three limitations of the existing toolkit: the lack of external choice, the inability to listen on multiple channels simultaneously, and the inability to handle timeouts on inputs. Whilst match types [5] were a promising initial direction of research, they addressed only one of t… view at source ↗
Figure 2
Figure 2. Figure 2: Syntax of the Extended -λ π ≤ calculus. The syntax of types is extended similarly, as shown in [PITH_FULL_IMAGE:figures/full_fig_p003_2.png] view at source ↗
Figure 3
Figure 3. Figure 3: Syntax of types for Extended -λ π ≤. Extended typing rules and semantics must build on the existing rules from [22]. As part of these rules, we expect to enforce conditions on the new constructs: for the timeout operation, we require that the first term is either a receive or a branch (the operations that can time out) and the second term is a lambda abstraction. For branching, we require: • Label distinct… view at source ↗
Figure 4
Figure 4. Figure 4: The state of a WaitingProcess, tracked by an atomic variable. Careful consideration is given to the interaction of multiple channels attempting to resolve the same Branch operation, and to races arising between timeouts and incoming messages. It is important to ensure that only one continuation (whether timeout or message-based) is triggered for each operation, regardless of the number of channels involved… view at source ↗
Figure 5
Figure 5. Figure 5: State machine representing Raft node states, adap [PITH_FULL_IMAGE:figures/full_fig_p007_5.png] view at source ↗
read the original 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.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit. Tearing a paper down is the easy half of reading it; the pith above is the substance, this is the friction.

Referee Report

2 major / 2 minor

Summary. The paper extends the Effpi framework for strongly-typed message-passing programs in Scala. It adds a branching operation realizing existential external choice (accepting messages over one or more channels, with label-dependent continuations) and a catch-timeout construct for handling absent messages. The authors claim these extensions increase expressiveness while preserving deadlock-freedom and liveness verification, which continues to be performed by encoding protocols into a CCS variant used by the existing compiler plugin. The claims are supported by several examples, including a full implementation of the Raft consensus algorithm.

Significance. If the encoding of the new operators into the existing CCS fragment is shown to be sound and property-preserving, the work would meaningfully broaden the class of verifiable protocols in Effpi, including realistic distributed algorithms such as Raft. The provision of concrete Scala examples is a positive step toward demonstrating practical utility.

major comments (2)
  1. [§3] §3 (Branching and Catch Timeout): The central claim that deadlock-freedom and liveness continue to hold for the extended language rests on an encoding of the new branching operator (existential choice over ≥1 channels with label-dependent continuations) and catch-timeout into the CCS fragment already handled by the compiler plugin. No translation rules, no definition of the encoding function, and no argument that the translation is faithful for the verified properties are supplied. This is load-bearing for all verification claims, including those made for the Raft example.
  2. [§4] §4 (Examples, Raft implementation): The Raft case study is presented as evidence that the enhanced expressiveness is useful and that verification still applies. However, without the missing encoding from §3, it is impossible to confirm that the deadlock/liveness checks performed by the plugin remain sound for the new constructs used in the Raft protocol.
minor comments (2)
  1. [§2] The syntax and typing rules for the multi-channel branching operation are introduced informally; a small formal grammar or typing judgment would improve clarity.
  2. [§4] Several code listings in the examples section contain minor formatting inconsistencies (e.g., indentation and line breaks) that reduce readability.

Simulated Author's Rebuttal

2 responses · 0 unresolved

Thank you for your thorough review and constructive feedback on our paper. We appreciate the recognition of the potential impact of our extensions to Effpi. Below, we address the major comments point by point and outline the revisions we will make.

read point-by-point responses

  1. Referee: [§3] §3 (Branching and Catch Timeout): The central claim that deadlock-freedom and liveness continue to hold for the extended language rests on an encoding of the new branching operator (existential choice over ≥1 channels with label-dependent continuations) and catch-timeout into the CCS fragment already handled by the compiler plugin. No translation rules, no definition of the encoding function, and no argument that the translation is faithful for the verified properties are supplied. This is load-bearing for all verification claims, including those made for the Raft example.

    Authors: We agree that the soundness of the encoding is essential to support the verification claims for the extended language and the Raft example. The submitted version focused on the language extensions and examples but omitted the detailed translation rules and the formal argument for property preservation. In the revised manuscript, we will add a new subsection in §3 defining the encoding function, providing explicit translation rules for the branching operator (including multi-channel existential choice and label-dependent continuations) and the catch-timeout construct into the CCS variant. We will also include an argument (or proof sketch) showing that the encoding preserves deadlock-freedom and liveness. revision: yes

  2. Referee: [§4] §4 (Examples, Raft implementation): The Raft case study is presented as evidence that the enhanced expressiveness is useful and that verification still applies. However, without the missing encoding from §3, it is impossible to confirm that the deadlock/liveness checks performed by the plugin remain sound for the new constructs used in the Raft protocol.

    Authors: The Raft implementation serves to demonstrate the practical utility of the new constructs. We acknowledge that its verification claims depend on the encoding's soundness. With the addition of the encoding details and preservation argument as outlined above, the verification for the Raft protocol will be substantiated. In the revision, we will cross-reference the encoding in the discussion of the Raft example and ensure that all used constructs are covered by the translation. revision: yes

Circularity Check

0 steps flagged

No significant circularity in Effpi extension derivation

full rationale

The paper defines new branching (multi-channel external choice with label-dependent continuations) and catch-timeout constructs as additive extensions to Effpi, then demonstrates them via examples including Raft. The preservation claim for deadlock-freedom and liveness rests on an asserted encoding into the existing CCS variant used by the compiler plugin. No quoted equation, definition, or self-citation reduces the central result to its own inputs by construction; the extension and verification transfer are presented as independent steps without self-definitional loops, fitted-input renaming, or load-bearing self-citation chains. The derivation chain remains self-contained against the prior Effpi framework.

Axiom & Free-Parameter Ledger

0 free parameters · 1 axioms · 0 invented entities

The central claim rests on the prior Effpi type system and its CCS encoding being extensible with the new constructs while preserving verification properties.

axioms (1)
  • domain assumption The existing Effpi type system and CCS encoding can be extended with branching and timeout operations while preserving deadlock-freedom and liveness verification.
    Invoked implicitly when claiming that the compiler plugin continues to verify the stated properties after the extension.

pith-pipeline@v0.9.0 · 5449 in / 1287 out tokens · 52514 ms · 2026-05-10T18:14:31.900135+00:00 · methodology

discussion (0)

Sign in with ORCID, Apple, or X to comment. Anyone can read and Pith papers without signing in.

Reference graph

Works this paper leans on

24 extracted references · 24 canonical work pages

  1. [1]

    Barwell, Ping Hou, Nobuko Y oshida & Fangyi Zhou (2 023): Designing Asynchronous Multi- party Protocols with Crash-Stop Failures

    Adam D. Barwell, Ping Hou, Nobuko Y oshida & Fangyi Zhou (2 023): Designing Asynchronous Multi- party Protocols with Crash-Stop Failures . In: 37th European Conference on Object-Oriented Programming (ECOOP 2023), Leibniz International Proceedings in Informatics (LIPIcs ) 263, Schloss Dagstuhl – Leibniz- Zentrum f¨ ur Informatik, Dagstuhl, Germany, pp. 1:1...

    work page doi:10.4230/lipics.ecoop.2023.1 2023

  2. [2]

    Willemse (2024): Modelling the Raft Distributed Consensus Pro- tocol in mCRL2

    Parth Bora, Pham Duc Minh & Tim A.C. Willemse (2024): Modelling the Raft Distributed Consensus Pro- tocol in mCRL2 . Electronic Proceedings in Theoretical Computer Science 399, pp. 7–20, doi: 10.4204/ eptcs.399.4

    work page 2024

  3. [3]

    Available at https://www

    Scala Developers (2021): Scala Documentation: Dependent Function Types . Available at https://www. scala-lang.org/api/3.3.7/docs/docs/reference/new-ty pes/dependent-function-types. html

    work page 2021

  4. [4]

    Available at https://www.scala-lang.org/ api/3.3.7/docs/docs/reference/contextual/givens.html

    Scala Developers (2021): Scala Documentation: Givens . Available at https://www.scala-lang.org/ api/3.3.7/docs/docs/reference/contextual/givens.html

    work page 2021

  5. [5]

    Available at https://www.scala-lang

    Scala Developers (2021): Scala Documentation: Match Types . Available at https://www.scala-lang. org/api/3.3.7/docs/docs/reference/new-types/match-t ypes.html

    work page 2021

  6. [6]

    Available at https://www.scala-lang

    Scala Developers (2021): Scala Documentation: Using Clauses . Available at https://www.scala-lang. org/api/3.3.7/docs/docs/reference/contextual/using-clauses.html

    work page 2021

  7. [7]

    Jan Friso Groote, Aad Mathijssen, Michel Reniers, Y aros lav Usenko & Muck van Weerdenburg (2007): The F ormal Specification Language mCRL2. In: Methods for Modelling Software Systems (MMOSS) , Dagstuhl 44 Branching Out: Existential External Choice in Effpi Seminar Proceedings (DagSemProc) 6351, Schloss Dagstuhl – Leibniz-Zentrum f¨ ur Informatik, Dagstuhl...

    work page doi:10.4230/dagsemproc.06351.12 2007

  8. [8]

    C. A. R. Hoare (1978): Communicating Sequential Processes. Commun. ACM 21(8), pp. 666–677, doi: 10. 1145/359576.359585

    work page arXiv 1978

  9. [9]

    In CONCUR ’93, 4th International Conference on Concurrency Theory, Hildesheim, Germany, August 23-26, 1993, Proceedings (Lecture Notes in Computer Science, Vol

    Kohei Honda (1993): Types for Dyadic Interaction . In Eike Best, editor: CONCUR’93 , Lecture Notes in Computer Science 715, Springer, Berlin, Heidelberg, pp. 509–523, doi: 10.1007/3-540-57208-2_35

    work page doi:10.1007/3-540-57208-2_35 1993

  10. [10]

    Ping Hou, Nicolas Lagaillardie & Nobuko Y oshida (2024) : Fearless Asynchronous Communications with Timed Multiparty Session Protocols . In: 38th European Conference on Object-Oriented Programming (ECOOP 2024), Leibniz International Proceedings in Informatics (LIPIcs ) 313, Schloss Dagstuhl – Leibniz- Zentrum f¨ ur Informatik, Dagstuhl, Germany, pp. 19:1–...

    work page doi:10.4230/lipics.ecoop.2024.19 2024

  11. [11]

    Heidi Howard & Richard Mortier (2020): Paxos vs Raft: Have we reached consensus on distributed con- sensus? Proceedings of the 7th Workshop on Principles and Practice o f Consistency for Distributed Data , doi:10.17863/CAM.51885

    work page doi:10.17863/cam.51885 2020

  12. [12]

    The part-time parliament.ACM Transactions on Computer Systems, 16 (2):133–169, 1998

    Leslie Lamport (1998): The Part-Time Parliament . ACM Transactions on Computer Systems 16(2), pp. 133–169, doi:10.1145/279227.279229

    work page doi:10.1145/279227.279229 1998

  13. [13]

    Available at https://doc.akka.io/libraries/ akka-core/current/typed/

    Inc Lightbend (2019): Akka Typed Documentation . Available at https://doc.akka.io/libraries/ akka-core/current/typed/

    work page 2019

  14. [14]

    Prentice-Hall international series in computer sci- ence, Prentice-Hall, New Y ork

    Robin Milner (1989): Communication and Concurrency . Prentice-Hall international series in computer sci- ence, Prentice-Hall, New Y ork

    work page 1989

  15. [15]

    Cambridge University Press, USA

    Robin Milner (1999): Communicating and Mobile Systems: The Pi-calculus . Cambridge University Press, USA

    work page 1999

  16. [16]

    In: USENIX A TC’14 , USENIX Association, USA, pp

    Diego Ongaro & John Ousterhout (2014): In Search of an Understandable Consensus Algorithm . In: USENIX A TC’14 , USENIX Association, USA, pp. 305–320. Available at https://www.usenix.org/ conference/atc14/technical-sessions/presentation/ongaro

    work page 2014

  17. [17]

    Available at https://benrobinson.dev/papers/places26-full.pdf

    Benjamin Robinson & Nobuko Y oshida (2026): Branching Out: Existential External Choice in Effpi (Full V ersion). Available at https://benrobinson.dev/papers/places26-full.pdf

    work page 2026

  18. [18]

    Roscoe (2000): The Theory and Practice of Concurrency

    Andrew W . Roscoe (2000): The Theory and Practice of Concurrency . Prentice Hall series in computer science, Prentice Hall, London

    work page 2000

  19. [19]

    In Mart´ ın Abadi & Alberto Lluch Lafuente, editors: Trustworthy Global Computing , Springer International Publishing, Cham, pp

    Neda Saeedloei & Gopal Gupta (2013): Timed Pi-calculus . In Mart´ ın Abadi & Alberto Lluch Lafuente, editors: Trustworthy Global Computing , Springer International Publishing, Cham, pp. 119–135, do i:10. 1007/978-3-319-05119-2_8

    work page 2013

  20. [20]

    In Shriram Krishna- murthi & Benjamin S

    Alceste Scalas & Nobuko Y oshida (2016): Lightweight Session Programming in Scala . In Shriram Krishna- murthi & Benjamin S. Lerner, editors: 30th European Conference on Object-Oriented Programming (ECOOP 2016), Leibniz International Proceedings in Informatics (LIPIcs) 56, Schloss Dagstuhl – Leibniz-Zentrum f¨ ur Informatik, Dagstuhl, Germany, pp. 21:1–21...

    work page doi:10.4230/lipics.ecoop.2016.21 2016

  21. [21]

    In: Proceedings of the Tenth ACM SIGPLAN Symposium on Scala , Scala ’19, Association for Computing Machinery, New Y ork, NY , USA, pp

    Alceste Scalas, Nobuko Y oshida & Elias Benussi (2019): Effpi: V erified Message-Passing Programs in Dotty. In: Proceedings of the Tenth ACM SIGPLAN Symposium on Scala , Scala ’19, Association for Computing Machinery, New Y ork, NY , USA, pp. 27–31, doi:10.1145/3337932.3338812

    work page doi:10.1145/3337932.3338812 2019

  22. [22]

    In: PLDI’19 , ACM, Phoenix AZ USA, pp

    Alceste Scalas, Nobuko Y oshida & Elias Benussi (2019): V erifying Message-Passing Programs with De- pendent Behavioural Types. In: PLDI’19 , ACM, Phoenix AZ USA, pp. 502–516, doi: 10.1145/3314221. 3322484

    work page doi:10.1145/3314221 2019

  23. [23]

    In: Distributed Computing and Internet Technology: 16th Inter national Conference, ICDCIT 2020, Proceedings , Springer-V erlag, Berlin, Heidelberg, pp

    Nobuko Y oshida & Lorenzo Gheri (2020): A V ery Gentle Introduction to Multiparty Session Types . In: Distributed Computing and Internet Technology: 16th Inter national Conference, ICDCIT 2020, Proceedings , Springer-V erlag, Berlin, Heidelberg, pp. 73–93, doi:10.1007/978-3-030-36987-3_5

    work page doi:10.1007/978-3-030-36987-3_5 2020

  24. [24]

    Less is More Revisited

    Nobuko Y oshida & Ping Hou (2024): Less is More Revisited. In Ana Cavalcanti & James Baxter, editors: The Practice of Formal Methods: Essays in Honour of Cliff Jones, Part II, Springer Nature Switzerland, Cham, pp. 268–291, doi: 10.1007/978-3-031-66673-5_14

    work page doi:10.1007/978-3-031-66673-5_14 2024