Less is More Revisited: Association with Global Protocols and Multiparty Sessions

Iona Kuhn; Nobuko Yoshida; Ping Hou

arxiv: 2402.16741 · v6 · pith:53RX6YDMnew · submitted 2024-02-26 · 💻 cs.PL

Less is More Revisited: Association with Global Protocols and Multiparty Sessions

Ping Hou , Nobuko Yoshida , Iona Kuhn This is my paper

Pith reviewed 2026-05-25 08:36 UTC · model grok-4.3

classification 💻 cs.PL

keywords multiparty session typesglobal protocolsend-point projectiontype soundnesssubject reductionassociation relationsession fidelitydeadlock freedom

0 comments

The pith

An association relation between global types and end-point projections establishes type soundness for multiparty session π-calculus.

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

The paper addresses concerns about flawed proofs of type safety in multiparty session types using end-point projection with mergeability. It proposes a new general proof technique for subject reduction in the multiparty session π-calculus based on an association relation between the behavioural semantics of a global type and its end-point projection. This relation guarantees that behavioural properties such as session fidelity, deadlock freedom, and liveness hold based on the global types. The work also includes detailed comparisons with existing MPST typing systems and their proof methods.

Core claim

We clarify this concern by proposing a new general proof technique for type soundness (subject reduction) of multiparty session π-calculus, which relies on an association relation between the behavioural semantics of a global type and its end-point projection. With this approach, behavioural properties, namely session fidelity, deadlock freedom, and liveness, are also guaranteed based on global types. Additionally, we provide detailed comparisons with existing MPST typing systems and discuss their respective proof methods for type soundness.

What carries the argument

The association relation between the behavioural semantics of a global type and its end-point projection that carries the proof of subject reduction.

If this is right

Subject reduction is proved for the multiparty session π-calculus using the association.
Session fidelity, deadlock freedom, and liveness are guaranteed from global types.
The approach works with end-point projection and addresses issues with mergeability.

Where Pith is reading between the lines

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

The method might simplify integration of MPST into more programming languages by providing a robust proof foundation.
It could be applied to verify correctness in distributed systems beyond the π-calculus.

Load-bearing premise

The association relation between the behavioural semantics of a global type and its end-point projection can be defined such that it supports subject reduction and the listed behavioral properties.

What would settle it

Finding a multiparty session protocol where the defined association relation does not preserve the reduction steps or behavioral properties would falsify the claim.

Figures

Figures reproduced from arXiv: 2402.16741 by Iona Kuhn, Nobuko Yoshida, Ping Hou.

**Figure 2.** Figure 2: Operational semantics of multiparty session [PITH_FULL_IMAGE:figures/full_fig_p004_2.png] view at source ↗

**Figure 3.** Figure 3: Standard structural congruence rules, where [PITH_FULL_IMAGE:figures/full_fig_p004_3.png] view at source ↗

**Figure 4.** Figure 4: Syntax of types. that a typing context obtained via projection ensures safety, deadlock-freedom, and liveness in § 3.5. 3.1 Global and Local Types The Multiparty Session Type (MPST) theory uses global types to provide a comprehensive overview of communication between roles, such as p, q, s, t, . . ., belonging to a set R. In contrast, it employs local types, which are obtained via projection from a global … view at source ↗

**Figure 5.** Figure 5: Global type reduction rules [PITH_FULL_IMAGE:figures/full_fig_p010_5.png] view at source ↗

**Figure 6.** Figure 6: Typing context reduction rules. Γ ′ , and Γ̸→s for its negation (i.e. there is no Γ ′ such that Γ →s Γ ′ ), and we denote →∗ s as the reflexive and transitive closure of →s; – Γ → Γ ′ holds iff Γ →s Γ ′ for some s: this means that Γ can progress via message transmission on any session. We write Γ→ iff Γ →Γ ′ for some Γ ′ , and Γ ̸→ for its negation, and we denote →∗ as the reflexive and transitive closure … view at source ↗

**Figure 7.** Figure 7: Typing rules for processes. In the diagram, the “safe” set (resp. “df” set, “live” set ) contains all typing contexts that are s-safe (resp. s-deadlock-free, s-live). The red set G encompasses all typing contexts associated with some global type for s. The negated implications stated in Thm. 4 are showcased in Ex. 8, Ex. 9, and Ex. 11 (below), respectively. Example 11 (Non-Associated Typing Context, origi… view at source ↗

read the original abstract

Ensuring correctness of communication in distributed systems remains challenging. To address this, Multiparty session types (MPST), initially introduced by Honda et al. [52, 53], offer a type discipline in which a programmer or architect specifies an overall view of communication as a global protocol (global type), and each distributed program is locally type-checked against its end-point projection. In practice, the MPST framework has been integrated into over 25 programming languages or tools. Ten years after the emergence of MPST, Scalas and Yoshida [84] discovered that existing proofs of type safety using end-point projection with mergeability are flawed, where the mergeability operator enlarges the typability of MPST end-point programs, admits easy implementation, and is more efficient than alternative approaches, including model checking. Nevertheless, following the result in [84], the soundness of end-point projection (with mergeability) has been interpreted in the literature as problematic. We clarify this concern by proposing a new general proof technique for type soundness (subject reduction) of multiparty session $\pi$-calculus, which relies on an association relation between the behavioural semantics of a global type and its end-point projection. With this approach, behavioural properties, namely session fidelity, deadlock freedom, and liveness, are also guaranteed based on global types. Additionally, we provide detailed comparisons with existing MPST typing systems and discuss their respective proof methods for type soundness.

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

The paper gives a new association relation to prove subject reduction for MPST endpoint projection without relying on the merge operator whose soundness was questioned earlier.

read the letter

The central contribution is a proof technique that uses an association between the behavioral semantics of a global type and its endpoint projections. This is meant to restore subject reduction and the usual behavioral guarantees (session fidelity, deadlock freedom, liveness) while keeping the practical advantages of projection with merge. The authors also lay out comparisons with other MPST systems and their respective soundness arguments. That is useful because the field has been carrying the Scalas-Yoshida observation for a decade and many tools still rely on the merge approach. The work is therefore aimed squarely at the known gap rather than adding yet another variant. The abstract is clear on the target and on what properties are recovered. The soft spot is that the provided text gives the claim and the high-level idea but no derivation steps, no definition of the association relation itself, and no counter-example checks. Without those, it is impossible to judge whether the relation is defined independently of the target properties or whether it actually closes the proof. If the full paper supplies the lemmas and they hold, the technique is a genuine alternative; if not, the claim stays at the level of a proposal. This paper is for people who work on the foundations of session types or who maintain MPST implementations. A reader who already knows the merge soundness issue will see the direct response and the comparison section. It is worth sending to referees because the problem it addresses is real, the proposed fix is stated precisely, and the subfield has enough active researchers to evaluate the details.

Referee Report

0 major / 2 minor

Summary. The paper claims that proofs of type safety for multiparty session types (MPST) using endpoint projection with mergeability are flawed, as identified by Scalas and Yoshida. It proposes a new general proof technique for subject reduction in the multiparty session π-calculus that relies on an association relation between the behavioural semantics of a global type and its endpoint projection. This technique is also claimed to guarantee session fidelity, deadlock freedom, and liveness. The manuscript includes detailed comparisons with existing MPST typing systems and their respective proof methods for type soundness.

Significance. If the association relation is shown to be well-defined and the proofs of subject reduction and the behavioural properties hold without gaps, the work would supply a general technique that directly addresses a known soundness concern in merge-based MPST projections. This is significant given the adoption of MPST in more than 25 languages and tools. The explicit comparisons with prior systems and proof methods provide additional value by situating the new technique in the existing literature.

minor comments (2)

[Abstract] Abstract: the claim that the association relation yields subject reduction would be easier to assess if the abstract briefly indicated one or two key properties of the relation (e.g., that it is defined from standard π-calculus semantics rather than from the target safety properties).
[Abstract] The statement that MPST has been integrated into 'over 25 programming languages or tools' would be strengthened by a citation or short list of representative systems.

Simulated Author's Rebuttal

0 responses · 0 unresolved

We thank the referee for the constructive summary and the recommendation of minor revision. The report accurately captures the paper's contribution in providing a general proof technique via the association relation to address known soundness issues with merge-based endpoint projection in MPST. No specific major comments were raised in the report, so we interpret the minor revision as pertaining to any editorial or presentational adjustments that may be requested by the editor.

Circularity Check

0 steps flagged

No significant circularity in derivation chain

full rationale

The paper proposes a new proof technique for subject reduction in multiparty session π-calculus that relies on defining an association relation between global-type behavioral semantics and endpoint projections. This relation is presented as a general method grounded in standard π-calculus semantics rather than being defined in terms of the target properties (session fidelity, deadlock freedom, liveness) it is used to establish. No self-definitional steps, fitted inputs renamed as predictions, or load-bearing self-citations that reduce the central claim to its own inputs are present in the abstract or stated claims. The technique directly targets a known prior flaw without circular reduction.

Axiom & Free-Parameter Ledger

0 free parameters · 1 axioms · 1 invented entities

The central claim rests on the existence and adequacy of a newly introduced association relation whose properties are not detailed in the abstract; standard π-calculus semantics are presupposed.

axioms (1)

standard math Standard behavioral semantics and projection rules for multiparty session π-calculus hold as background
The association relation is defined over these semantics (abstract).

invented entities (1)

Association relation between global-type semantics and endpoint projections no independent evidence
purpose: To establish subject reduction and behavioral properties without mergeability
New construct introduced to link global and local behaviors; no independent evidence supplied in abstract.

pith-pipeline@v0.9.0 · 5786 in / 1303 out tokens · 27907 ms · 2026-05-25T08:36:24.508719+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/AbsoluteFloorClosure.lean reality_from_one_distinction unclear

?

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

We clarify this concern by proposing a new general proof technique for type soundness (subject reduction) of multiparty session π-calculus, which relies on an association relation between the behavioural semantics of a global type and its end-point projection.
IndisputableMonolith/Foundation/ArithmeticFromLogic.lean LogicNat recovery unclear

?

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

G ⊑s Γ … dom(ΓG) = {s[p] | p ∈ roles(G)}, and ∀p ∈ roles(G) : G ↾ p ⩽ Γ (s[p])
IndisputableMonolith/Foundation/BranchSelection.lean branch_selection unclear

?

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

Theorem 3 (Safety, Deadlock-Freedom, and Liveness by Association)

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

39 extracted references · 39 canonical work pages

[1]

In: 33rd International Conference on Concurrency Theory

Barwell, A., Scalas, A., Yoshida, N., Zhou, F.: Generalised Multiparty Session Types with Crash-Stop Failures. In: 33rd International Conference on Concurrency Theory. LIPIcs, vol. 243, pp. 35:1–35:25. Dagstuhl (2022).https://doi.org/10. 4230/LIPIcs.CONCUR.2022.35

work page 2022
[2]

LMCS 12(2) (2016)

Bernardi, G., Hennessy, M.: Using higher-order contracts to model session types. LMCS 12(2) (2016). https://doi.org/10.2168/LMCS-12(2:10)2016

work page doi:10.2168/lmcs-12(2:10)2016 2016
[3]

In: Proceedings of ESOP 2007

Carbone, M., Honda, K., Yoshida, N.: Structured Communication-Centred Pro- gramming for Web Services. In: Proceedings of ESOP 2007. LNCS, vol. 4421, pp. 2–17. Springer (2007).https://doi.org/10.1007/978-3-540-71316-6_2

work page doi:10.1007/978-3-540-71316-6_2 2007
[4]

In: Formal Methods for Multicore Programming (2015)

Coppo, M., Dezani-Ciancaglini, M., Padovani, L., Yoshida, N.: A Gentle Introduc- tion to Multiparty Asynchronous Session Types. In: Formal Methods for Multicore Programming (2015). https://doi.org/10.1007/978-3-319-18941-3_4

work page doi:10.1007/978-3-319-18941-3_4 2015
[5]

MSCS760(2015)

Coppo, M., Dezani-Ciancaglini, M., Yoshida, N., Padovani, L.: Global progress for dynamically interleaved multiparty sessions. MSCS760(2015). https://doi.org/ 10.1017/S0960129514000188

work page doi:10.1017/s0960129514000188 2015
[6]

In: 40th Interna- tional Colloquium on Automata, Languages and Programming

Deniélou, P.M., Yoshida, N.: Multiparty Compatibility in Communicating Au- tomata: Characterisation and Synthesis of Global Session Types. In: 40th Interna- tional Colloquium on Automata, Languages and Programming. LNCS, vol. 7966, pp. 174–186. Springer (2013).https://doi.org/10.1007/978-3-642-39212-2_18

work page doi:10.1007/978-3-642-39212-2_18 2013
[7]

ACM Transactions on Computational Logic Volume 24, Issue 2(14), 1–73 (2023).https://doi.org/10.1145/3568422

Ghilezan, S., Pantović, J., Prokić, I., Scalas, A., Yoshida, N.: Precise Subtyping for Asynchronous Multiparty Sessions. ACM Transactions on Computational Logic Volume 24, Issue 2(14), 1–73 (2023).https://doi.org/10.1145/3568422

work page doi:10.1145/3568422 2023
[8]

In: 2021 36th Annual ACM/IEEE Sym- posium on Logic in Computer Science (LICS)

Glabbeek, R.v., Höfner, P., Horne, R.: Assuming just enough fairness to make session types complete for lock-freedom. In: 2021 36th Annual ACM/IEEE Sym- posium on Logic in Computer Science (LICS). pp. 1–13 (2021).https://doi.org/ 10.1109/LICS52264.2021.9470531

work page doi:10.1109/lics52264.2021.9470531 2021
[9]

Web Services Choreography Working Group: http://w3.org/2002/ws/chor/ (2003)

work page 2002
[10]

In: Wand, I., Milner, R

Gurd, J.R., Jones, C.B.: The global-yet-personal information system. In: Wand, I., Milner, R. (eds.) Computing Tomorrow, pp. 127–157. Cambridge University Press (1996). https://doi.org/10.1017/CBO9780511605611

work page doi:10.1017/cbo9780511605611 1996
[11]

In: Brodie, M.L., Mylopoulos, J., Schmidt, J.W

Hewitt, C., de Jong, P.: Open systems. In: Brodie, M.L., Mylopoulos, J., Schmidt, J.W. (eds.) On Conceptual Modelling: Perspectives from Artificial Intelligence, Databases, and Programming Languages, pp. 147–164. Springer (1984).https: //doi.org/10.1007/978-1-4612-5196-5_6

work page doi:10.1007/978-1-4612-5196-5_6 1984
[12]

In: ICDCIT

Honda, K., Mukhamedov, A., Brown, G., Chen, T.C., Yoshida, N.: Scribbling in- teractions with a formal foundation. In: ICDCIT. LNCS, vol. 6536, pp. 55–75. Springer (2011). https://doi.org/10.1007/978-3-642-19056-8_4

work page doi:10.1007/978-3-642-19056-8_4 2011
[13]

In: POPL (2008)

Honda, K., Yoshida, N., Carbone, M.: Multiparty asynchronous session types. In: POPL (2008). https://doi.org/10.1145/1328438.1328472, full version in [14]

work page doi:10.1145/1328438.1328472 2008
[14]

Honda, K., Yoshida, N., Carbone, M.: Multiparty Asynchronous Session Types. J. ACM63(1) (2016). https://doi.org/10.1145/2827695

work page doi:10.1145/2827695 2016
[15]

In: International Con- ference on Compiler Construction

Miu, A., Ferreira, F., Yoshida, N., Zhou, F.: Communication-Safe Web Program- ming in TypeScript with Routed Multiparty Session Types. In: International Con- ference on Compiler Construction. pp. 94–106. CC (2021).https://doi.org/10. 1145/3446804.3446854

work page arXiv 2021
[16]

org/html/rfc6749 (2012) Less is More Revisited 23

OAuth Working Group: RFC 6749: OAuth 2.0 framework.http://tools.ietf. org/html/rfc6749 (2012) Less is More Revisited 23

work page 2012
[17]

The MIT Press, 1st edn

Pierce, B.C.: Types and Programming Languages. The MIT Press, 1st edn. (2002), https://dl.acm.org/doi/abs/10.5555/509043

work page doi:10.5555/509043 2002
[18]

Cambridge Univer- sity Press (2011).https://doi.org/10.1017/CBO9780511777110

Sangiorgi, D.: Introduction to Bisimulation and Coinduction. Cambridge Univer- sity Press (2011).https://doi.org/10.1017/CBO9780511777110

work page doi:10.1017/cbo9780511777110 2011
[19]

Scalas, A., Yoshida, N.: Less is More: Multiparty Session Types Revisited. Proc. ACM Program. Lang. 3(POPL), 30:1–30:29 (Jan 2019).https://doi.org/10. 1145/3290343

work page 2019
[20]

SIGPLAN OOPS Mess.5(2), 3–12 (April 1993)

Tokoro, M.: The society of objects. SIGPLAN OOPS Mess.5(2), 3–12 (April 1993). https://doi.org/10.1145/260304.260305

work page doi:10.1145/260304.260305 1993
[21]

In: Distributed Computing and Internet Technology - ICDCIT 2020

Yoshida, N., Gheri, L.: A very gentle introduction to multiparty session types. In: Distributed Computing and Internet Technology - ICDCIT 2020. Lecture Notes in Computer Science, vol. 11969, pp. 73–93. Springer (2020).https://doi.org/10. 1007/978-3-030-36987-3_5

work page 2020
[22]

In: Trustworthy Global Computing

Yoshida, N., Hu, R., Neykova, R., Ng, N.: The Scribble Protocol Language. In: Trustworthy Global Computing. LNCS, vol. 8358, pp. 22–41. Springer (2013). https://doi.org/10.1007/978-3-319-05119-2_3

work page doi:10.1007/978-3-319-05119-2_3 2013
[23]

In: 23rd International Sym- posium on Fundamentals of Computation Theory

Yoshida, N., Zhou, F., Ferreira, F.: Communicating Finite State Machines and an Extensible Toolchain for Multiparty Session Types. In: 23rd International Sym- posium on Fundamentals of Computation Theory. LNCS, vol. 12867, pp. 18–35. Springer (2021). https://doi.org/10.1007/978-3-030-86593-1_2 24 N. Yoshida and P. Hou A Proofs for § 3 With regard to recur...

work page doi:10.1007/978-3-030-86593-1_2 2021
[24]

T ⩽ unf(T ). Proof. 1. By [Sub-µR] if T = µt.T ′. Otherwise, by reflexivity (Lem. 3). 2. By [Sub-µL] if T = µt.T ′. Otherwise, by reflexivity (Lem. 3). Less is More Revisited 25 Lemma 7. Given a collection of mergable local typesTi (i ∈ I). For allj ∈ I, Tj ⩽ d i∈I Ti holds. Proof. By constructing a relationR = (Tj, d i∈I Ti) j ∈ I , and showing that R ⊆⩽...

work page
[25]

If U ⩽ p⊕{mi(Si).Ti}i∈I, then unf(U ) = p⊕ m′ j(S′ j).T ′ j j∈J, and I ⊆ J, and ∀i ∈ I : mi = m′ i, Si ⩽ S′ i and T ′ i ⩽ Ti

work page
[26]

If U ⩽ p&{mi(Si).Ti}i∈I, then unf(U ) = p& m′ j(S′ j).T ′ j j∈J, and J ⊆ I, and ∀i ∈ J : mi = m′ i, S′ i ⩽ Si and T ′ i ⩽ Ti. Proof. By Lems. 1 and 6, the transitivity of subtyping, and Def. 4 ([Sub-&], [Sub- ⊕]). A.3 Semantics of Global Types Lemma 12. G α − →G′ iff unf(G) α − →G′. Proof. By inverting or applying[GR-µ] when necessary. Lemma 13 (Progress ...

work page
[27]

If Γ s[p]:q⊕mk(Sk) − − − − − − − − →Γ ′, then unf(Γ (s[p])) = q⊕{mi(Si).Ti}i∈I, k ∈ I, and Γ ′(s[p]) = Tk

work page
[28]

If Γ s[q]:p&mk(Sk) − − − − − − − − →Γ ′, then unf(Γ (s[q])) = p&{mi(Si).Ti}i∈I, k ∈ I, and Γ ′(s[q]) = Tk. Proof. By applying and inverting[Γ -⊕], [Γ -&], and [Γ -µ] (when necessary). Lemma 17 (Determinism of Typing Context Reduction).If Γ α − →Γ ′ and Γ α − →Γ ′′, then Γ ′ = Γ ′′. Proof. By induction on typing context reductions. Lemma 18. If Γ →s Γ ′, t...

work page
[29]

If Γ s[p]:q⊕mk(Sk) − − − − − − − − →Γ ′, then for any channel with rolec ∈ dom(Γ ) with c ̸= s[p], Γ (c) = Γ ′(c)

work page
[30]

If Γ s[q]:p&mk(Sk) − − − − − − − − →Γ ′, then for any channel with rolec ∈ dom(Γ ) with c ̸= s[q], Γ (c) = Γ ′(c)

work page
[31]

If Γ s[p][q]m − − − − →Γ ′, then for any channel with rolec ∈ dom(Γ ) with c ̸= s[p] and c ̸= s[q], Γ (c) = Γ ′(c). Proof. By induction on typing context reductions. Less is More Revisited 27 A.5 Relating Semantics Proposition 1. G ⊑s Γ if and only ifG{µt.G/t} ⊑ s Γ. Proof. By Lem. 6. Proposition 2. G ⊑s Γ if and only ifunf(G) ⊑s Γ. Proof. By applying Pro...

work page
[32]

If unf(Γ (s[p])) = q⊕{mi(Si).Ti}i∈I, then either (a) unf(G) = p→q: {mi(S′ i).Gi}i∈I ′, whereI ⊆ I ′, and for alli ∈ I : mi = mi, Si ⩽ S′ i, and Gi ↾ p ⩽ Ti; or, (b) unf(G) = s→t: mj(S′ j).Gj j∈J, where for allj ∈ J : Gj ↾ p ⩽ Γ (s[p]), with p ̸= s and p ̸= t

work page
[33]

If unf(Γ (s[p])) = q&{mi(Si).Ti}i∈I, then either (a) unf(G) = q→p: {mi(S′ i).Gi}i∈I ′, where I ′ ⊆ I, and for alli ∈ I ′ : mi = mi, S′ i ⩽ Si, and Gi ↾ p ⩽ Ti; or, (b) unf(G) = s→t: mj(S′ j).Gj j∈J, where for allj ∈ J : Gj ↾ p ⩽ Γ (s[p]), with p ̸= s and p ̸= t

work page
[34]

If unf(Γ (s[p])) = end, then p /∈ roles(G). Proof. Thanks to Lem. 1, we do not need to consider top-level recursions, items (1), (2), and (3) follow from Def. 9, Lem. 2, and Lem. 22. Lemma 25 (Simultaneous Inversions of Association). Let G ⊑s Γ. If unf(Γ (s[p])) = q⊕{mi(Si).Ti}i∈Ip and unf(Γ (s[q])) = p&{mi(S′ i).T ′ i }i∈Iq , then either

work page
[35]

unf(G) = p→q: {mi(S′′ i ).Gi}i∈I, where Ip ⊆ I ⊆ Iq, ∀i ∈ Ip : Si ⩽ S′′ i , ∀i ∈ I : S′′ i ⩽ S′ i, ∀i ∈ Ip : Gi ↾ p ⩽ Ti, and ∀i ∈ I : Gi ↾ q ⩽ T ′ i; or,

work page
[36]

unf(G) = s→t: mj(S′′ j ).Gj j∈J, where for all j ∈ J : Gj ↾ p ⩽ Γ (s[p]), Gj ↾ q ⩽ Γ (s[q]), and {p, q} ∩ {s, t} = ∅. Proof. By combining cases (1) and (2) from Lem. 24. Note that case 1(a) is incompatible with case 2(b), since 2(b) requires thatp ̸= s. Similarly, case 1(b) is incompatible with case 2(a). Theorem 1 (Soundness of Association). Given associ...

work page
[37]

P = Q | R and P ′ = Q′ | R and Q → Q′

work page
[38]

P = (νs′) Q and P ′ = (νs′) Q′ and Q → Q′

work page
[39]

Therefore, here we focus on case 2

P = def D in Q and P ′ = def D in Q′ and Q → Q′ Less is More Revisited 39 Cases 1 and 3 are easily proved using the induction hypothesis. Therefore, here we focus on case 2. ∃Γ ′, G such that G ⊑s′ Γ ′ s′ ̸∈ Γ Θ · Γ , Γ′ ⊢ Q Θ · Γ ⊢ P [T-G-ν] (by 2 and Lem. 34(4)) (39) ∃Γ ′′, Γ ′′′ such that    s′ ̸∈ Γ ′′ Γ →∗ Γ ′′ Γ ′ →∗ Γ ′′′ ∀s ∈ Γ ′′ : ∃G′′...

work page

[1] [1]

In: 33rd International Conference on Concurrency Theory

Barwell, A., Scalas, A., Yoshida, N., Zhou, F.: Generalised Multiparty Session Types with Crash-Stop Failures. In: 33rd International Conference on Concurrency Theory. LIPIcs, vol. 243, pp. 35:1–35:25. Dagstuhl (2022).https://doi.org/10. 4230/LIPIcs.CONCUR.2022.35

work page 2022

[2] [2]

LMCS 12(2) (2016)

Bernardi, G., Hennessy, M.: Using higher-order contracts to model session types. LMCS 12(2) (2016). https://doi.org/10.2168/LMCS-12(2:10)2016

work page doi:10.2168/lmcs-12(2:10)2016 2016

[3] [3]

In: Proceedings of ESOP 2007

Carbone, M., Honda, K., Yoshida, N.: Structured Communication-Centred Pro- gramming for Web Services. In: Proceedings of ESOP 2007. LNCS, vol. 4421, pp. 2–17. Springer (2007).https://doi.org/10.1007/978-3-540-71316-6_2

work page doi:10.1007/978-3-540-71316-6_2 2007

[4] [4]

In: Formal Methods for Multicore Programming (2015)

Coppo, M., Dezani-Ciancaglini, M., Padovani, L., Yoshida, N.: A Gentle Introduc- tion to Multiparty Asynchronous Session Types. In: Formal Methods for Multicore Programming (2015). https://doi.org/10.1007/978-3-319-18941-3_4

work page doi:10.1007/978-3-319-18941-3_4 2015

[5] [5]

MSCS760(2015)

Coppo, M., Dezani-Ciancaglini, M., Yoshida, N., Padovani, L.: Global progress for dynamically interleaved multiparty sessions. MSCS760(2015). https://doi.org/ 10.1017/S0960129514000188

work page doi:10.1017/s0960129514000188 2015

[6] [6]

In: 40th Interna- tional Colloquium on Automata, Languages and Programming

Deniélou, P.M., Yoshida, N.: Multiparty Compatibility in Communicating Au- tomata: Characterisation and Synthesis of Global Session Types. In: 40th Interna- tional Colloquium on Automata, Languages and Programming. LNCS, vol. 7966, pp. 174–186. Springer (2013).https://doi.org/10.1007/978-3-642-39212-2_18

work page doi:10.1007/978-3-642-39212-2_18 2013

[7] [7]

ACM Transactions on Computational Logic Volume 24, Issue 2(14), 1–73 (2023).https://doi.org/10.1145/3568422

Ghilezan, S., Pantović, J., Prokić, I., Scalas, A., Yoshida, N.: Precise Subtyping for Asynchronous Multiparty Sessions. ACM Transactions on Computational Logic Volume 24, Issue 2(14), 1–73 (2023).https://doi.org/10.1145/3568422

work page doi:10.1145/3568422 2023

[8] [8]

In: 2021 36th Annual ACM/IEEE Sym- posium on Logic in Computer Science (LICS)

Glabbeek, R.v., Höfner, P., Horne, R.: Assuming just enough fairness to make session types complete for lock-freedom. In: 2021 36th Annual ACM/IEEE Sym- posium on Logic in Computer Science (LICS). pp. 1–13 (2021).https://doi.org/ 10.1109/LICS52264.2021.9470531

work page doi:10.1109/lics52264.2021.9470531 2021

[9] [9]

Web Services Choreography Working Group: http://w3.org/2002/ws/chor/ (2003)

work page 2002

[10] [10]

In: Wand, I., Milner, R

Gurd, J.R., Jones, C.B.: The global-yet-personal information system. In: Wand, I., Milner, R. (eds.) Computing Tomorrow, pp. 127–157. Cambridge University Press (1996). https://doi.org/10.1017/CBO9780511605611

work page doi:10.1017/cbo9780511605611 1996

[11] [11]

In: Brodie, M.L., Mylopoulos, J., Schmidt, J.W

Hewitt, C., de Jong, P.: Open systems. In: Brodie, M.L., Mylopoulos, J., Schmidt, J.W. (eds.) On Conceptual Modelling: Perspectives from Artificial Intelligence, Databases, and Programming Languages, pp. 147–164. Springer (1984).https: //doi.org/10.1007/978-1-4612-5196-5_6

work page doi:10.1007/978-1-4612-5196-5_6 1984

[12] [12]

In: ICDCIT

Honda, K., Mukhamedov, A., Brown, G., Chen, T.C., Yoshida, N.: Scribbling in- teractions with a formal foundation. In: ICDCIT. LNCS, vol. 6536, pp. 55–75. Springer (2011). https://doi.org/10.1007/978-3-642-19056-8_4

work page doi:10.1007/978-3-642-19056-8_4 2011

[13] [13]

In: POPL (2008)

Honda, K., Yoshida, N., Carbone, M.: Multiparty asynchronous session types. In: POPL (2008). https://doi.org/10.1145/1328438.1328472, full version in [14]

work page doi:10.1145/1328438.1328472 2008

[14] [14]

Honda, K., Yoshida, N., Carbone, M.: Multiparty Asynchronous Session Types. J. ACM63(1) (2016). https://doi.org/10.1145/2827695

work page doi:10.1145/2827695 2016

[15] [15]

In: International Con- ference on Compiler Construction

Miu, A., Ferreira, F., Yoshida, N., Zhou, F.: Communication-Safe Web Program- ming in TypeScript with Routed Multiparty Session Types. In: International Con- ference on Compiler Construction. pp. 94–106. CC (2021).https://doi.org/10. 1145/3446804.3446854

work page arXiv 2021

[16] [16]

org/html/rfc6749 (2012) Less is More Revisited 23

OAuth Working Group: RFC 6749: OAuth 2.0 framework.http://tools.ietf. org/html/rfc6749 (2012) Less is More Revisited 23

work page 2012

[17] [17]

The MIT Press, 1st edn

Pierce, B.C.: Types and Programming Languages. The MIT Press, 1st edn. (2002), https://dl.acm.org/doi/abs/10.5555/509043

work page doi:10.5555/509043 2002

[18] [18]

Cambridge Univer- sity Press (2011).https://doi.org/10.1017/CBO9780511777110

Sangiorgi, D.: Introduction to Bisimulation and Coinduction. Cambridge Univer- sity Press (2011).https://doi.org/10.1017/CBO9780511777110

work page doi:10.1017/cbo9780511777110 2011

[19] [19]

Scalas, A., Yoshida, N.: Less is More: Multiparty Session Types Revisited. Proc. ACM Program. Lang. 3(POPL), 30:1–30:29 (Jan 2019).https://doi.org/10. 1145/3290343

work page 2019

[20] [20]

SIGPLAN OOPS Mess.5(2), 3–12 (April 1993)

Tokoro, M.: The society of objects. SIGPLAN OOPS Mess.5(2), 3–12 (April 1993). https://doi.org/10.1145/260304.260305

work page doi:10.1145/260304.260305 1993

[21] [21]

In: Distributed Computing and Internet Technology - ICDCIT 2020

Yoshida, N., Gheri, L.: A very gentle introduction to multiparty session types. In: Distributed Computing and Internet Technology - ICDCIT 2020. Lecture Notes in Computer Science, vol. 11969, pp. 73–93. Springer (2020).https://doi.org/10. 1007/978-3-030-36987-3_5

work page 2020

[22] [22]

In: Trustworthy Global Computing

Yoshida, N., Hu, R., Neykova, R., Ng, N.: The Scribble Protocol Language. In: Trustworthy Global Computing. LNCS, vol. 8358, pp. 22–41. Springer (2013). https://doi.org/10.1007/978-3-319-05119-2_3

work page doi:10.1007/978-3-319-05119-2_3 2013

[23] [23]

In: 23rd International Sym- posium on Fundamentals of Computation Theory

Yoshida, N., Zhou, F., Ferreira, F.: Communicating Finite State Machines and an Extensible Toolchain for Multiparty Session Types. In: 23rd International Sym- posium on Fundamentals of Computation Theory. LNCS, vol. 12867, pp. 18–35. Springer (2021). https://doi.org/10.1007/978-3-030-86593-1_2 24 N. Yoshida and P. Hou A Proofs for § 3 With regard to recur...

work page doi:10.1007/978-3-030-86593-1_2 2021

[24] [24]

T ⩽ unf(T ). Proof. 1. By [Sub-µR] if T = µt.T ′. Otherwise, by reflexivity (Lem. 3). 2. By [Sub-µL] if T = µt.T ′. Otherwise, by reflexivity (Lem. 3). Less is More Revisited 25 Lemma 7. Given a collection of mergable local typesTi (i ∈ I). For allj ∈ I, Tj ⩽ d i∈I Ti holds. Proof. By constructing a relationR = (Tj, d i∈I Ti) j ∈ I , and showing that R ⊆⩽...

work page

[25] [25]

If U ⩽ p⊕{mi(Si).Ti}i∈I, then unf(U ) = p⊕ m′ j(S′ j).T ′ j j∈J, and I ⊆ J, and ∀i ∈ I : mi = m′ i, Si ⩽ S′ i and T ′ i ⩽ Ti

work page

[26] [26]

If U ⩽ p&{mi(Si).Ti}i∈I, then unf(U ) = p& m′ j(S′ j).T ′ j j∈J, and J ⊆ I, and ∀i ∈ J : mi = m′ i, S′ i ⩽ Si and T ′ i ⩽ Ti. Proof. By Lems. 1 and 6, the transitivity of subtyping, and Def. 4 ([Sub-&], [Sub- ⊕]). A.3 Semantics of Global Types Lemma 12. G α − →G′ iff unf(G) α − →G′. Proof. By inverting or applying[GR-µ] when necessary. Lemma 13 (Progress ...

work page

[27] [27]

If Γ s[p]:q⊕mk(Sk) − − − − − − − − →Γ ′, then unf(Γ (s[p])) = q⊕{mi(Si).Ti}i∈I, k ∈ I, and Γ ′(s[p]) = Tk

work page

[28] [28]

If Γ s[q]:p&mk(Sk) − − − − − − − − →Γ ′, then unf(Γ (s[q])) = p&{mi(Si).Ti}i∈I, k ∈ I, and Γ ′(s[q]) = Tk. Proof. By applying and inverting[Γ -⊕], [Γ -&], and [Γ -µ] (when necessary). Lemma 17 (Determinism of Typing Context Reduction).If Γ α − →Γ ′ and Γ α − →Γ ′′, then Γ ′ = Γ ′′. Proof. By induction on typing context reductions. Lemma 18. If Γ →s Γ ′, t...

work page

[29] [29]

If Γ s[p]:q⊕mk(Sk) − − − − − − − − →Γ ′, then for any channel with rolec ∈ dom(Γ ) with c ̸= s[p], Γ (c) = Γ ′(c)

work page

[30] [30]

If Γ s[q]:p&mk(Sk) − − − − − − − − →Γ ′, then for any channel with rolec ∈ dom(Γ ) with c ̸= s[q], Γ (c) = Γ ′(c)

work page

[31] [31]

If Γ s[p][q]m − − − − →Γ ′, then for any channel with rolec ∈ dom(Γ ) with c ̸= s[p] and c ̸= s[q], Γ (c) = Γ ′(c). Proof. By induction on typing context reductions. Less is More Revisited 27 A.5 Relating Semantics Proposition 1. G ⊑s Γ if and only ifG{µt.G/t} ⊑ s Γ. Proof. By Lem. 6. Proposition 2. G ⊑s Γ if and only ifunf(G) ⊑s Γ. Proof. By applying Pro...

work page

[32] [32]

If unf(Γ (s[p])) = q⊕{mi(Si).Ti}i∈I, then either (a) unf(G) = p→q: {mi(S′ i).Gi}i∈I ′, whereI ⊆ I ′, and for alli ∈ I : mi = mi, Si ⩽ S′ i, and Gi ↾ p ⩽ Ti; or, (b) unf(G) = s→t: mj(S′ j).Gj j∈J, where for allj ∈ J : Gj ↾ p ⩽ Γ (s[p]), with p ̸= s and p ̸= t

work page

[33] [33]

If unf(Γ (s[p])) = q&{mi(Si).Ti}i∈I, then either (a) unf(G) = q→p: {mi(S′ i).Gi}i∈I ′, where I ′ ⊆ I, and for alli ∈ I ′ : mi = mi, S′ i ⩽ Si, and Gi ↾ p ⩽ Ti; or, (b) unf(G) = s→t: mj(S′ j).Gj j∈J, where for allj ∈ J : Gj ↾ p ⩽ Γ (s[p]), with p ̸= s and p ̸= t

work page

[34] [34]

If unf(Γ (s[p])) = end, then p /∈ roles(G). Proof. Thanks to Lem. 1, we do not need to consider top-level recursions, items (1), (2), and (3) follow from Def. 9, Lem. 2, and Lem. 22. Lemma 25 (Simultaneous Inversions of Association). Let G ⊑s Γ. If unf(Γ (s[p])) = q⊕{mi(Si).Ti}i∈Ip and unf(Γ (s[q])) = p&{mi(S′ i).T ′ i }i∈Iq , then either

work page

[35] [35]

unf(G) = p→q: {mi(S′′ i ).Gi}i∈I, where Ip ⊆ I ⊆ Iq, ∀i ∈ Ip : Si ⩽ S′′ i , ∀i ∈ I : S′′ i ⩽ S′ i, ∀i ∈ Ip : Gi ↾ p ⩽ Ti, and ∀i ∈ I : Gi ↾ q ⩽ T ′ i; or,

work page

[36] [36]

unf(G) = s→t: mj(S′′ j ).Gj j∈J, where for all j ∈ J : Gj ↾ p ⩽ Γ (s[p]), Gj ↾ q ⩽ Γ (s[q]), and {p, q} ∩ {s, t} = ∅. Proof. By combining cases (1) and (2) from Lem. 24. Note that case 1(a) is incompatible with case 2(b), since 2(b) requires thatp ̸= s. Similarly, case 1(b) is incompatible with case 2(a). Theorem 1 (Soundness of Association). Given associ...

work page

[37] [37]

P = Q | R and P ′ = Q′ | R and Q → Q′

work page

[38] [38]

P = (νs′) Q and P ′ = (νs′) Q′ and Q → Q′

work page

[39] [39]

Therefore, here we focus on case 2

P = def D in Q and P ′ = def D in Q′ and Q → Q′ Less is More Revisited 39 Cases 1 and 3 are easily proved using the induction hypothesis. Therefore, here we focus on case 2. ∃Γ ′, G such that G ⊑s′ Γ ′ s′ ̸∈ Γ Θ · Γ , Γ′ ⊢ Q Θ · Γ ⊢ P [T-G-ν] (by 2 and Lem. 34(4)) (39) ∃Γ ′′, Γ ′′′ such that    s′ ̸∈ Γ ′′ Γ →∗ Γ ′′ Γ ′ →∗ Γ ′′′ ∀s ∈ Γ ′′ : ∃G′′...

work page