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

Recognition: 2 theorem links

· Lean Theorem

Modelling Distributed Applications with Mixed-Choice Stateful Typestates

Francisco Parrinha (NOVA LINCS , NOVA FCT , Lisbon , Portugal) , Jo\~ao Mota (NOVA LINCS , Ant\'onio Ravara (NOVA LINCS

Authors on Pith no claims yet

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

classification 💻 cs.PL

keywords typestatesdistributed protocolsruntime monitoringmixed sessionsstateful typestatesquantitative constraintssession types

0 comments

The pith

Typestates are extended with mutable internal state, mixed sessions, and expected action ratios to model quantitative constraints and concurrent behaviors in distributed protocols.

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

The paper proposes extending typestates to better handle distributed systems by adding support for quantitative constraints and concurrent actions. Traditional typestates struggle with expressing things like the number of acknowledgements needed or handling simultaneous input and output in a state. The solution adds an internal mutable state, mixed sessions for concurrent operations, and expected ratios of actions monitored at runtime to detect deviations. This is shown through examples like an acknowledgement protocol and a voting protocol for consensus. If correct, this allows runtime verification where static methods fall short due to network uncertainties.

Core claim

We present a probabilistic runtime solution extending typestates with an internal mutable state for the expression of quantitative constraints, mixed sessions to represent concurrent input and output actions, and expected ratios for the number of actions in a state, with monitoring semantics to detect deviations from an expected behaviour at runtime.

What carries the argument

Mixed-choice stateful typestates that incorporate internal mutable state for quantitative constraints, mixed sessions for concurrent actions, and expected ratios with monitoring.

If this is right

An acknowledgement protocol can be modelled with a participant sending multiple messages while waiting for responses using mixed sessions.
A voting protocol can use mutable state to track quorums while enforcing expected message volume distributions via ratios.
Runtime monitoring detects deviations from expected behaviour in distributed protocols where static verification is insufficient.
The approach supports modelling input and output operations concurrently in the same state.

Where Pith is reading between the lines

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

This could enable better design of other distributed consensus mechanisms by allowing probabilistic checks at runtime.
Integration with existing session type tools might help developers catch errors in asynchronous handlers earlier.
Testing in real networks could reveal if the monitoring overhead remains acceptable for large scale applications.

Load-bearing premise

That the proposed extensions integrate cleanly into typestate frameworks and that runtime monitoring of expected ratios can reliably detect meaningful deviations in real distributed environments without high overhead or false positives.

What would settle it

Deploying the monitoring in a live distributed system and measuring if it accurately flags deviations with minimal false positives and acceptable performance cost.

Figures

Figures reproduced from arXiv: 2604.06874 by Ant\'onio Ravara (NOVA LINCS, Francisco Parrinha (NOVA LINCS, Jo\~ao Mota (NOVA LINCS, Lisbon, NOVA FCT, Portugal).

**Figure 2.** Figure 2: Textual typestates for the AlternatingBitProtoc [PITH_FULL_IMAGE:figures/full_fig_p003_2.png] view at source ↗

**Figure 3.** Figure 3: Graphical typestates for the BitVoteProtocol. [PITH_FULL_IMAGE:figures/full_fig_p003_3.png] view at source ↗

**Figure 4.** Figure 4: The internal state for the Leader. acknowledgements and the number of retries left; n and k, as read-only, to represent the number of peers and the starting number of retries, respectively. The map ‘Preds’ stores predicates. These are assigned to actions in a typestate. Each predicate is evaluated whenever the associated action is executed, triggering the corresponding transition when their evaluation yiel… view at source ↗

**Figure 5.** Figure 5: Textual typestate for the Leader. Each action contains now three parameters: a ratio, a list with keys of ‘Assigns’ representing ‘preassignments’ and a list with keys belonging to ‘Preds’ for each predicate. We also add a list with ‘postassignments’ after the destinations. For example, the predicates P1 and P2 check whether all acknowledgements have been received or all retries have been spent. Either c… view at source ↗

**Figure 6.** Figure 6: Textual typestate for the Peer [PITH_FULL_IMAGE:figures/full_fig_p004_6.png] view at source ↗

read the original abstract

Distributed systems have become increasingly prevalent in the software industry. Due to their intrinsic complexity, much research has focused on the verification of their behaviour. An active research line is around behaviour models that capture these protocols - e.g., session types, or typestates - allowing their static verification. Correctly designing distributed protocols is not trivial. Their communication behaviour is typically implicitly defined via asynchronous message handlers, making errors harder to detect until execution. While typestates can ease the design process by explicitly defining correct sequences of operations, they struggle in two ways: they lack the expressiveness to define quantitative constraints that govern distributed protocols (i.e., number of acknowledgements for a quorum); and they assume strict sequencing of operations, failing to capture concurrent input/output actions in a state, typical of the distributed setting. Furthermore, runtime network failures cannot be statically verified. We present a probabilistic runtime solution extending typestates with: (i) an internal mutable state for the expression of quantitative constraints; (ii) mixed sessions to represent concurrent input and output actions; (iii) expected ratios for the number of actions in a state, with monitoring semantics to detect deviations from an expected behaviour at runtime. We demonstrate the suitability of our solution with two examples that motivated our approach: an acknowledgement protocol with a participant that sends several messages while waiting for a response, effectively modelling input and output operations in a state; and a voting protocol whose participants try to achieve consensus on a single bit using a quorum, thus, requiring an internal mutable state, while respecting a pre-defined distribution for the volume of exchanged messages.

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.

Desk Editor's Note private letter to a colleague

This paper sketches typestate extensions for mutable state, mixed sessions, and ratio-based runtime monitoring to handle quantitative and concurrent aspects in distributed protocols, but stays high-level with only examples and no formal or empirical support.

read the letter

The main thing to know is that the authors extend typestates with an internal mutable state for counting things like acknowledgments, mixed sessions that allow concurrent input and output in one state, and probabilistic expected ratios monitored at runtime to catch deviations. They motivate this with an acknowledgement protocol and a voting/quorum protocol. That combination targets real gaps in how typestates handle distributed settings where strict sequencing and lack of quantitative tracking are problems. The examples are useful for showing why these features matter in practice. What the paper does well is clearly stating the limitations of existing typestates for concurrency and quantitative constraints, then demonstrating the ideas on two protocols that actually need them. The writing is straightforward about the motivation. The soft spots are more substantial. There are no formal semantics, type rules, or proofs of soundness. No implementation details or evaluation data appear to show overhead, false positive rates, or how the monitoring integrates without breaking existing typestate guarantees. The claims about clean integration and reliable detection rest entirely on the high-level descriptions and examples. This is aimed at researchers working on session types and typestates for distributed systems verification. A reader already familiar with the area might pick up the proposed directions, but anyone wanting solid results or reusable formal machinery will find it thin. I would send it to peer review because the identified gaps are genuine and the target features address them directly, even if the current version needs substantial expansion on the formal and practical side to be convincing.

Referee Report

2 major / 1 minor

Summary. The manuscript proposes extending typestates for distributed applications by adding (i) internal mutable state to express quantitative constraints, (ii) mixed sessions to represent concurrent input and output actions within a state, and (iii) expected ratios of actions together with monitoring semantics that detect runtime deviations from expected behavior. These extensions are motivated by limitations of standard typestates in handling quantitative aspects (e.g., quorums) and concurrent I/O, and are illustrated via two concrete protocols: an acknowledgement protocol in which a participant issues multiple messages while awaiting a response, and a voting protocol that achieves consensus via quorum while respecting a pre-defined message distribution.

Significance. If the extensions can be equipped with a sound formal semantics and the monitoring mechanism can be shown to operate with acceptable overhead, the work would meaningfully increase the expressiveness of typestate-based modeling for distributed systems by bridging static sequencing with runtime quantitative checks. The two motivating examples are well-chosen and clearly demonstrate the targeted shortcomings of existing typestates.

major comments (2)

[Abstract] Abstract: the central claim that the three extensions constitute a 'probabilistic runtime solution' with 'monitoring semantics' rests entirely on high-level description of the two protocols; no formal type rules, operational semantics, or monitoring transition rules are supplied, which is load-bearing for any assertion that the extensions integrate cleanly or that deviations can be reliably detected.
[Voting protocol example] Voting protocol example: the need for mutable state to track quorum progress and for expected ratios is stated, yet the manuscript supplies neither the update rules for the internal state nor the definition of the monitoring predicate that would detect deviations, leaving the practical feasibility of the runtime component unverified.

minor comments (1)

[Abstract] The abstract lists the three extensions as (i), (ii), (iii) but does not explicitly map each feature to the corresponding limitation mentioned in the preceding paragraph, which would improve readability.

Simulated Author's Rebuttal

2 responses · 0 unresolved

We thank the referee for the constructive feedback and for recognizing the potential significance of our proposed extensions. We address each major comment below and commit to revisions that strengthen the formal foundations of the work.

read point-by-point responses

Referee: [Abstract] Abstract: the central claim that the three extensions constitute a 'probabilistic runtime solution' with 'monitoring semantics' rests entirely on high-level description of the two protocols; no formal type rules, operational semantics, or monitoring transition rules are supplied, which is load-bearing for any assertion that the extensions integrate cleanly or that deviations can be reliably detected.

Authors: We agree that the manuscript currently presents the extensions primarily through high-level descriptions and illustrative protocols rather than supplying complete formal type rules, operational semantics, or monitoring transition rules. This was a deliberate choice to first establish the motivation and applicability via the acknowledgement and voting examples. To substantiate the central claims, we will revise the manuscript by adding a dedicated formal semantics section. This will include: (i) extended type rules incorporating mutable state and mixed sessions, (ii) operational semantics defining transitions for concurrent I/O and state updates, and (iii) monitoring transition rules that specify how deviations from expected action ratios are detected at runtime. These additions will demonstrate clean integration and reliable detection. revision: yes
Referee: [Voting protocol example] Voting protocol example: the need for mutable state to track quorum progress and for expected ratios is stated, yet the manuscript supplies neither the update rules for the internal state nor the definition of the monitoring predicate that would detect deviations, leaving the practical feasibility of the runtime component unverified.

Authors: The referee is correct that the voting protocol example motivates mutable state for quorum tracking and expected ratios for message distribution but does not supply the concrete update rules or monitoring predicate. In the revised manuscript we will add these definitions explicitly. We will specify the state-update rules (e.g., how vote counts are incremented on message receipt and how quorum thresholds are checked) and the monitoring predicate (a runtime check that compares observed action ratios against the declared expected distribution and raises a deviation alert when the difference exceeds a configurable tolerance). This will verify the practical feasibility of the runtime monitoring component. revision: yes

Circularity Check

0 steps flagged

No significant circularity detected

full rationale

The paper is a proposal for extending typestates with internal mutable state, mixed sessions for concurrent I/O, and ratio-based runtime monitoring, illustrated via two protocol examples (acknowledgement and voting/quorum). No derivation chain, equations, fitted parameters, or predictions are presented that could reduce to self-definition or self-citation. The central claims concern expressiveness and runtime detection suitability, which remain independent of any internal reduction. This is a standard non-circular modeling contribution.

Axiom & Free-Parameter Ledger

0 free parameters · 2 axioms · 3 invented entities

The approach rests on standard typestate foundations plus new constructs for state, mixed choice, and monitoring; no free parameters are specified.

axioms (2)

domain assumption Typestates can be extended with mutable internal state and mixed input/output without breaking static verification properties
Invoked when proposing the extension to handle quantitative and concurrent aspects.
domain assumption Expected action ratios can be predefined and monitored at runtime to detect deviations from correct protocol behavior
Central to the probabilistic monitoring semantics.

invented entities (3)

mixed sessions no independent evidence
purpose: Represent concurrent input and output actions within a single state
Introduced to overcome strict sequencing limitation of standard typestates.
internal mutable state no independent evidence
purpose: Express quantitative constraints such as quorum sizes or acknowledgement counts
New mechanism for handling counts that standard typestates lack.
expected ratios no independent evidence
purpose: Define and monitor probabilistic distribution of actions for runtime deviation detection
Provides the probabilistic runtime verification component.

pith-pipeline@v0.9.0 · 5618 in / 1444 out tokens · 47704 ms · 2026-05-10T18:20:28.702987+00:00 · methodology

discussion (0)

Lean theorems connected to this paper

Citations machine-checked in the Pith Canon. Every link opens the source theorem in the public Lean library.

IndisputableMonolith/Foundation/RealityFromDistinction.lean reality_from_one_distinction unclear

?

unclear
Relation between the paper passage and the cited Recognition theorem.

We present a probabilistic runtime solution extending typestates with: (i) an internal mutable state for the expression of quantitative constraints; (ii) mixed sessions to represent concurrent input and output actions; (iii) expected ratios for the number of actions in a state, with monitoring semantics...
IndisputableMonolith/Cost/FunctionalEquation.lean washburn_uniqueness_aczel unclear

?

unclear
Relation between the paper passage and the cited Recognition theorem.

By assigning ratios to each action in a state, the generated monitors can use a frequentist approach to infer the runtime correctness...

What do these tags mean?

matches: The paper's claim is directly supported by a theorem in the formal canon.
supports: The theorem supports part of the paper's argument, but the paper may add assumptions or extra steps.
extends: The paper goes beyond the formal theorem; the theorem is a base layer rather than the whole result.
uses: The paper appears to rely on the theorem as machinery.
contradicts: The paper's claim conflicts with a theorem or certificate in the canon.
unclear: Pith found a possible connection, but the passage is too broad, indirect, or ambiguous to say the theorem truly supports the claim.

Reference graph

Works this paper leans on

13 extracted references · 11 canonical work pages

[1]

Lorenzo Bacchiani, Mario Bravetti, Marco Giunti, Jo˜ ao Mota & Ant´ onio Ravara (2022): A Java typestate checker supporting inheritance . Sci. Comput. Program. 221, p. 102844, doi: 10.1016/J.SCICO.2022. 102844

work page doi:10.1016/j.scico.2022 2022
[2]

Lorenzo Bacchiani, Mario Bravetti, Marco Giunti, Jo˜ ao Mota & Ant´ onio Ravara (2024): Behavioural Up/down Casting F or Statically Typed Languages. In Jonathan Aldrich & Guido Salvaneschi, editors: 38th European Conference on Object-Oriented Programming, ECOO P 2024, Vienna, Austria, September 16-20, 2024, LIPIcs 313, Schloss Dagstuhl - Leibniz-Zentrum f...

work page doi:10.4230/lipics 2024
[3]

Christian Bartolo Burl` o, Adrian Francalanza & Alceste Scalas (2020): T owards a Hybrid V eriﬁcation Meth- odology for Communication Protocols (Short Paper) . In Alexey Gotsman & Ana Sokolova, editors: Formal Techniques for Distributed Objects, Components, and Systems - 40th IFIP WG 6.1 International Conference, FORTE 2020, Held as Part of the 15th Inter...

work page doi:10.1007/978-3-030-50086-3_13 2020
[4]

Christian Bartolo Burl` o, Adrian Francalanza, Alceste Scalas, Catia Trubiani & Emilio Tuosto (2021): T o- wards Probabilistic Session-Type Monitoring. In Ferruccio Damiani & Ornela Dardha, editors: Coordination Models and Languages - 23rd IFIP WG 6.1 International Confer ence, COORDINA TION 2021, Held as Part of the 16th International Federated Conferenc...

work page doi:10.1007/978-3-030-78142-2_7 2021
[5]

V asconcelos (20 22): Mixed sessions

Filipe Casal, Andreia Mordido & V asco T. V asconcelos (20 22): Mixed sessions . Theor. Comput. Sci. 897, pp. 23–48, doi: 10.1016/J.TCS.2021.08.005

work page doi:10.1016/j.tcs.2021.08.005 2021
[6]

Ankush Das, Di Wang & Jan Hoffmann (2023): Probabilistic Resource-Aware Session Types. Proc. ACM Program. Lang. 7(POPL), pp. 1925–1956, doi: 10.1145/3571259

work page doi:10.1145/3571259 2023
[7]

Raymond Hu, Nobuko Y oshida & Kohei Honda (2008): Session-Based Distributed Programming in Java . In Jan Vitek, editor: ECOOP 2008 - Object-Oriented Programming, 22nd European Co nference, Paphos, Cyprus, July 7-11, 2008, Proceedings , Lecture Notes in Computer Science 5142, Springer, pp. 516–541, doi:10.1007/978-3-540-70592-5_22

work page doi:10.1007/978-3-540-70592-5_22 2008
[8]

Hans H¨ uttel, Ivan Lanese, V asco T. V asconcelos, Lu´ ıs Caires, Marco Carbone, Pierre-Malo Deni´ elou, Di- mitris Mostrous, Luca Padovani, Ant´ onio Ravara, Emilio Tuosto, Hugo Torres Vieira & Gianluigi Zavattaro (2016): F oundations of Session Types and Behavioural Contracts. ACM Comput. Surv. 49(1), pp. 3:1–3:36, doi:10.1145/2873052

work page doi:10.1145/2873052 2016
[9]

Jo˜ ao Mota, Marco Giunti & Ant´ onio Ravara (2021): Java Typestate Checker . In Ferruccio Damiani & Ornela Dardha, editors: Coordination Models and Languages - 23rd IFIP WG 6.1 Interna tional Conference, COORDINA TION 2021, Held as Part of the 16th International Federated Conference on Distributed Comput- ing Techniques, DisCoTec 2021, V alletta, Malta, ...

work page doi:10.1007/978-3-030-78142-2_8 2021
[10]

Typestate: A Programming Language Concept for Enhancing Software Reliability,

Robert E. Strom & Shaula Y emini (1986): Typestate: A Programming Language Concept for Enhancing Software Reliability. IEEE Trans. Software Eng. 12(1), pp. 157–171, doi: 10.1109/TSE.1986.6312929

work page doi:10.1109/tse.1986.6312929 1986
[11]

Dagstuhl Artifacts Ser

Dawit Legesse Tirore, Jesper Bengtson & Marco Carbone ( 2025): Multiparty Asynchronous Session Types: A Mechanised Proof of Subject Reduction (Artifact) . Dagstuhl Artifacts Ser. 11(2), pp. 3:1–3:5, doi: 10.4230/ DARTS.11.2.3

2025
[12]

V asconcelos (2012): Fundamentals of session types

V asco T. V asconcelos (2012): Fundamentals of session types . Inf. Comput. 217, pp. 52–70, doi: 10.1016/ J.IC.2012.05.002

2012
[13]

Fangyi Zhou, Francisco Ferreira, Raymond Hu, Rumyana N eykova & Nobuko Y oshida (2020): Statically veriﬁed reﬁnements for multiparty protocols . Proc. ACM Program. Lang. 4(OOPSLA), pp. 148:1–148:30, doi:10.1145/3428216

work page doi:10.1145/3428216 2020