arxiv: 2604.10646 · v1 · submitted 2026-04-12 · 💻 cs.PL

Recognition: unknown

Denotational reasoning for asynchronous multiparty session types

Dylan McDermott, Nobuko Yoshida

Authors on Pith no claims yet

Pith reviewed 2026-05-10 15:32 UTC · model grok-4.3

classification 💻 cs.PL

keywords asynchronous multiparty session typesdenotational semanticscomputational effectsgradingasynchronous subtypingcommunication safetydeadlock freedom

0 comments

The pith

Modelling message passing as a graded computational effect gives the first denotational semantics for asynchronous multiparty session types with precise subtyping.

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

This paper develops a denotational semantics for asynchronous multiparty session types that supports precise asynchronous subtyping. The semantics models non-blocking message sends and allows reasoning about optimizations like reordering messages. By treating message-passing as a computational effect and using grading to track it, the approach ensures that typed programs remain safe, deadlock-free, and live even after such optimizations. It also shows adequacy with respect to an operational calculus for call-by-value asynchronous communication.

Core claim

The paper's core contribution is the construction of a denotational model for asynchronous multiparty session types in which asynchronous subtyping is precise, achieved by interpreting session types via graded effects that capture the non-blocking nature of message passing. This model permits formal verification that communication optimisations, particularly those involving reordering, preserve the key properties of communication safety, deadlock freedom, and liveness.

What carries the argument

Grading applied to the computational effect of asynchronous message-passing, which tracks effects to interpret session types denotationally.

If this is right

Communication safety holds for programs even when messages are reordered.
Deadlock-freedom is guaranteed under the asynchronous semantics.
Liveness properties are preserved despite communication optimisations.
The denotational model is adequate for the call-by-value asynchronous message-passing calculus.

Where Pith is reading between the lines

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

The graded effect view may let session type systems inherit proof techniques from effect systems in other domains.
Adequacy results could be used to transfer operational properties to denotational reasoning in related calculi.
The approach suggests that other concurrency models with non-blocking sends might admit similar graded interpretations.

Load-bearing premise

Message-passing can be accurately modelled as a computational effect to which grading applies.

What would settle it

An asynchronous multiparty session type program that the semantics deems safe and live but that actually deadlocks or violates safety after a message reordering optimisation.

Figures

Figures reproduced from arXiv: 2604.10646 by Dylan McDermott, Nobuko Yoshida.

**Figure 1.** Figure 1: Operational semantics of SafeMP. configuration C = (ρ, t, σ) consists of a (receive) queue ρ, closed computation t, and a (send) queue σ. The queue ρ contains messages yet to be consumed by t, while the queue σ contains messages that have been produced by t. Our operational semantics is defined at the bottom of [PITH_FULL_IMAGE:figures/full_fig_p006_1.png] view at source ↗

**Figure 2.** Figure 2: Four inductively defined relations and predicates on multiparty session types we do have U <: T. This is because we have T ′ <: T ′ and U ′ <: U ′ (subtyping is reflexive by Lemma 7 below). To satisfy (1), it is therefore enough to note that T q!cont⟨int⟩ ,−−−−−−→ U ′ and T q!stop⟨bool⟩ ,−−−−−−−→ U ′ . To satisfy (4), it enough to note that U p?success⟨int⟩ ,−−−−−−−−→ T ′ and U p?error⟨bool⟩ ,−−−−−−−−→ T ′… view at source ↗

**Figure 3.** Figure 3: Typing of values, computations, and configurations in SafeMP contexts because t is a closed computation; the rules ensure that T is a closed session type. The [CBase] rule uses our computation typing judgement with empty contexts (we write · for an empty context). The intuition for [CSend] is that the configuration in the conclusion is sending a message to p; we therefore need to ensure that the type U per… view at source ↗

**Figure 4.** Figure 4: Interpretation of SafeMP values, computations and configurations a function ϕ(f): Jb1K × · · · × JbnK → N (Jb ′ K)T[θ] ; we write JΦKθ for the set of such function environments. For computations, we interpret each derivation of Θ #Φ#Γ ⊢ t : b #T as a function JtKθ : JΦKθ ×JΓK → N (JbK)T[θ] . This is defined in [PITH_FULL_IMAGE:figures/full_fig_p020_4.png] view at source ↗

**Figure 5.** Figure 5: Definitions of projection and of full merging of multiparty session types Example 23. In the context of Example 1, the computation t implements a participant r as part of a global protocol described by the following global type G; we can associate to t the session type G ↾ r. G = p → r:    success⟨int⟩.r→q: ( cont⟨int⟩. end stop⟨bool⟩. end error⟨bool⟩.r→q: stop⟨bool⟩. end G↾p = r ⊕ ( success⟨int⟩.end… view at source ↗

**Figure 6.** Figure 6: Four inductively defined relations and predicates on session trees Definition 82. Asynchronous subtyping is the largest relation <: on session trees, such that the following hold when T <: U. 1. If T = p ⊕i∈I ℓi⟨bi⟩.Ti, then for every i ∈ I, there is some Ui such that U p!ℓi⟨bi⟩ ,−−−−→ Ui and Ti <: Ui. 2. If T = p &i∈I ℓi⟨bi⟩.Ti, then Recvsp(U). 3. If U = p ⊕i∈I ℓi⟨bi⟩.Ui, then Sendsp(T). 4. If U = p &i∈I … view at source ↗

read the original abstract

We provide the first denotational semantics for asynchronous multiparty session types with precise asynchronous subtyping. Our semantics enables us to reason about asynchronous message-passing, in which message-sending is non-blocking. It enables us to prove the correctness of communication optimisations, in particular, those involving reordering of messages. Our development crucially relies on modelling message-passing as a computational effect. We apply grading, a paradigm for tracking computational effects, to asynchronous message-passing, demonstrating that multiparty session typing can be viewed as an instance of grading. We demonstrate the utility of our model by showing that it forms an adequate denotational semantics for a call-by-value asynchronous message-passing calculus, that ensures communication safety, deadlock-freedom and liveness in the presence of communication optimisations.

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 the first graded denotational semantics for async MPST that supports precise asynchronous subtyping and proves safety under message reordering.

read the letter

This paper supplies the first denotational semantics for asynchronous multiparty session types that includes precise asynchronous subtyping. It does so by modeling message passing as a graded computational effect, which lets the authors treat session typing as an instance of the grading paradigm. The work shows that this semantics is adequate for a call-by-value asynchronous message-passing calculus. From that they derive that the types ensure communication safety, deadlock-freedom, and liveness even when communication optimizations reorder messages. That is the practical payoff. The approach is clean. By using grading they avoid having to build a custom denotational model from scratch and instead leverage existing machinery for effects. The adequacy result ties the semantics back to the operational behavior, which is the right check to make. I do not see major gaps in the high-level argument. The central claim that the graded model captures the asynchronous behavior and supports subtyping without losing the safety properties holds up in the construction they describe. The reliance on the effect model is explicit and seems well-motivated rather than a hidden assumption. This paper is for people already working in session types or effect systems who want a denotational foundation for asynchronous protocols. A reader familiar with multiparty session types and graded modalities will find the technical development useful and potentially extensible. It deserves serious refereeing. The novelty of the combination and the adequacy proof make it worth expert scrutiny even if some details need tightening in revision.

Referee Report

0 major / 2 minor

Summary. The manuscript presents the first denotational semantics for asynchronous multiparty session types (MPST) that supports precise asynchronous subtyping. Message-passing is modeled as a graded computational effect, allowing reasoning about non-blocking sends and communication optimizations such as message reordering. The semantics is shown to be adequate for a call-by-value asynchronous message-passing calculus and to guarantee communication safety, deadlock-freedom, and liveness under these optimizations.

Significance. If the adequacy and safety results hold, the work is significant for providing the first denotational account of asynchronous MPST with subtyping that explicitly handles asynchrony and reordering. By framing MPST as an instance of the grading paradigm for effects, it creates a bridge between session types and effect systems that may enable further cross-applications. The paper supplies an adequacy result for the denotational model, which is a concrete strength.

minor comments (2)

[Abstract] Abstract: the phrase 'precise asynchronous subtyping' is used without a brief contrast to existing synchronous or imprecise variants; a short clarifying sentence would help readers new to the area.
[Introduction] The modeling of message-passing as an effect is described as crucial; ensure the introduction or §2 makes explicit why this modeling choice is independently motivated rather than tailored solely to the target calculus.

Simulated Author's Rebuttal

0 responses · 0 unresolved

We thank the referee for their positive summary and significance assessment of our work on the denotational semantics for asynchronous multiparty session types. The recommendation for minor revision is noted, and we will incorporate any editorial improvements in the revised version.

Circularity Check

0 steps flagged

No significant circularity; adequacy is a non-trivial proof, not a definitional match

full rationale

The paper constructs a graded denotational model by treating asynchronous message-passing as a computational effect and applies the existing grading paradigm to obtain a semantics for multiparty session types. It then proves adequacy with respect to a separate operational calculus. Adequacy is a standard, non-trivial theorem that must be established rather than assumed by construction; the model is not defined to be identical to the operational behavior. No self-definitional equations, fitted parameters renamed as predictions, or load-bearing self-citations that reduce the central claims to unverified inputs appear in the derivation. The development is self-contained against external benchmarks of effect grading and session-type safety.

Axiom & Free-Parameter Ledger

0 free parameters · 1 axioms · 0 invented entities

The central claim rests on standard denotational semantics for effects and the adequacy of treating asynchronous message passing as a graded computational effect; these are domain assumptions drawn from prior effect-system literature.

axioms (1)

standard math Standard axioms of denotational semantics and graded effect systems
The development builds on existing frameworks for modeling computational effects via grading.

pith-pipeline@v0.9.0 · 5422 in / 1166 out tokens · 48404 ms · 2026-05-10T15:32:17.648010+00:00 · methodology

discussion (0)

Reference graph

Works this paper leans on

146 extracted references

[1]

Logical relations for session-typed concurrency, 2023

Stephanie Balzer, Farzaneh Derakhshan, Robert Harper, and Yue Yao. Logical relations for session-typed concurrency, 2023

2023
[2]

Effect-dependent transforma- tions for concurrent programs

Nick Benton, Martin Hofmann, and Vivek Nigam. Effect-dependent transforma- tions for concurrent programs. InProceedings of the 18th International Symposium on Principles and Practice of Declarative Programming, pages 188–201, 2016

2016
[3]

Abstract subtypingforasynchronousmultipartysessions

Laura Bocchi, Andy King, Maurizio Murgia, and Simon Thompson. Abstract subtypingforasynchronousmultipartysessions. InPatriciaBouyerandJacovande Pol, editors,36th International Conference on Concurrency Theory, CONCUR 2025, August 26-29, 2025, Aarhus, Denmark, volume 348 ofLIPIcs, pages 10:1– 10:19. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2025

2025
[4]

Internal object actions

Francis Borceux, George Janelidze, and G Max Kelly. Internal object actions. Comment. Math. Univ. Carolin., 46(2):235–255, 2005

2005
[5]

Undecidability of asynchronous session subtyping.Information and Computation, 256:300–320, 2017

Mario Bravetti, Marco Carbone, and Gianluigi Zavattaro. Undecidability of asynchronous session subtyping.Information and Computation, 256:300–320, 2017

2017
[6]

On the boundary be- tween decidability and undecidability of asynchronous session subtyping.Theoret- ical Computer Science, 722:19–51, 2018

Mario Bravetti, Marco Carbone, and Gianluigi Zavattaro. On the boundary be- tween decidability and undecidability of asynchronous session subtyping.Theoret- ical Computer Science, 722:19–51, 2018

2018
[7]

Pérez, Frank Pfenning, and Bernardo Toninho

Luís Caires, Jorge A. Pérez, Frank Pfenning, and Bernardo Toninho. Behavioral polymorphism and parametricity in session-based communication. InESOP, vol- ume 7792 ofLNCS, pages 330–349. Springer, 2013

2013
[8]

Session types as intuitionistic linear propositions

Luís Caires and Frank Pfenning. Session types as intuitionistic linear propositions. InProceedings of CONCUR 2010, volume 6269 ofLNCS, pages 222–236. Springer, 2010

2010
[9]

Two sides of the same coin: session types and game semantics: a synchronous side and an asynchronous side.Proc

Simon Castellan and Nobuko Yoshida. Two sides of the same coin: session types and game semantics: a synchronous side and an asynchronous side.Proc. ACM Program. Lang., 3(POPL), January 2019

2019
[10]

Event structure semantics for multiparty sessions.J

Ilaria Castellani, Mariangiola Dezani-Ciancaglini, and Paola Giannini. Event structure semantics for multiparty sessions.J. Log. Algebraic Methods Program., 131:100844, 2023

2023
[11]

Global types andevent structuresemanticsfor asynchronousmultiparty sessions.Fundam

Ilaria Castellani, Mariangiola Dezani-Ciancaglini, and Paola Giannini. Global types andevent structuresemanticsfor asynchronousmultiparty sessions.Fundam. Informaticae, 192(1):1–75, 2024

2024
[12]

CAMP: cost-aware multiparty session protocols.Proc

David Castro-Perez and Nobuko Yoshida. CAMP: cost-aware multiparty session protocols.Proc. ACM Program. Lang., 4(OOPSLA):155:1–155:30, 2020

2020
[13]

Deadlock-free asynchronous message reordering in Rust with multiparty session types

Zak Cutner, Nobuko Yoshida, and Martin Vassor. Deadlock-free asynchronous message reordering in Rust with multiparty session types. In Jaejin Lee, Kunal Agrawal, and Michael F. Spear, editors,PPoPP ’22: 27th ACM SIGPLAN Sym- posium on Principles and Practice of Parallel Programming, Seoul, Republic of Korea, April 2 - 6, 2022, pages 246–261. ACM, 2022

2022
[14]

A denotational approach to re- lease/acquire concurrency

Yotam Dvir, Ohad Kammar, and Ori Lahav. A denotational approach to re- lease/acquire concurrency. InEuropean Symposium on Programming, pages 121–
[15]

Two-sorted algebraic decompositions of brookes’s shared-state denotational semantics

Yotam Dvir, Ohad Kammar, Ori Lahav, and Gordon Plotkin. Two-sorted algebraic decompositions of brookes’s shared-state denotational semantics. InFoundations of Software Science and Computation Structures: 28th International Conference, FoSSaCS 2025, Held as Part of the International Joint Conferences on Theory and Practice of Software, ETAPS 2025, Hamilton...

2025
[16]

Completeness of Asynchronous Session Tree Subtyping in Coq

Burak Ekici and Nobuko Yoshida. Completeness of Asynchronous Session Tree Subtyping in Coq. In15th International Conference on Interactive Theorem Prov- ing, 2024, Tbilisi, Georgia, volume 309 ofLIPIcs, pages 6:1–6:20. Schloss Dagstuhl - Leibniz-Zentrum f"ur Informatik, 2024

2024
[17]

Precise subtyping for synchronous multiparty sessions.Journal of Logical and Algebraic Methods in Programming, 104:127–173, 2019

Silvia Ghilezan, Svetlana Jakšić, Jovanka Pantović, Alceste Scalas, and Nobuko Yoshida. Precise subtyping for synchronous multiparty sessions.Journal of Logical and Algebraic Methods in Programming, 104:127–173, 2019

2019
[18]

Precise subtyping for asynchronous multiparty sessions.ACM Trans

Silvia Ghilezan, Jovanka Pantović, Ivan Prokić, Alceste Scalas, and Nobuko Yoshida. Precise subtyping for asynchronous multiparty sessions.ACM Trans. Comput. Logic, 24(2), nov 2023

2023
[19]

Types for dyadic interaction

Kohei Honda. Types for dyadic interaction. In Eike Best, editor,CONCUR’93, pages 509–523. Springer, 1993

1993
[20]

Language Prim- itives and Type Discipline for Structured Communication-Based Programming

Kohei Honda, Vasco Thudichum Vasconcelos, and Makoto Kubo. Language Prim- itives and Type Discipline for Structured Communication-Based Programming. In Chris Hankin, editor,Programming Languages and Systems - ESOP’98, 7th Euro- pean Symposium on Programming, Held as Part of the European Joint Conferences on the Theory and Practice of Software, ETAPS’98, L...

1998
[21]

Multiparty asynchronous session types.Journal of the ACM, 63(1):9:1–9:67, 2016

Kohei Honda, Nobuko Yoshida, and Marco Carbone. Multiparty asynchronous session types.Journal of the ACM, 63(1):9:1–9:67, 2016

2016
[22]

Multiparty GV: functional multiparty session types with certified deadlock freedom.Proc

Jules Jacobs, Stephanie Balzer, and Robbert Krebbers. Multiparty GV: functional multiparty session types with certified deadlock freedom.Proc. ACM Program. Lang., 6(ICFP):466–495, 2022

2022
[23]

Algebraic foundations for effect-dependent optimisations

Ohad Kammar and Gordon D Plotkin. Algebraic foundations for effect-dependent optimisations. InProceedings of the 39th annual ACM SIGPLAN-SIGACT sym- posium on Principles of programming languages, pages 349–360, 2012

2012
[24]

Parametric effect monads and semantics of effect systems

Shin-ya Katsumata. Parametric effect monads and semantics of effect systems. In Proc. of 41st Ann. ACM SIGPLAN-SIGACT Symp. on Principles of Programming Languages, POPL ’14, San Diego, CA, USA, January 20-21, 2014, pages 633–645. ACM, 2014

2014
[25]

Adequacy for algebraic effects revisited.Proceedings of the ACM on Programming Languages, 9(OOPSLA1):927–955, 2025

GA Kavvos. Adequacy for algebraic effects revisited.Proceedings of the ACM on Programming Languages, 9(OOPSLA1):927–955, 2025

2025
[26]

On the relative ex- pressiveness of higher-order session processes.Information and Computation, 268:104433, 2019

Dimitrios Kouzapas, Jorge A Pérez, and Nobuko Yoshida. On the relative ex- pressiveness of higher-order session processes.Information and Computation, 268:104433, 2019

2019
[27]

Pérez, and Nobuko Yoshida

Dimitrios Kouzapas, Jorge A. Pérez, and Nobuko Yoshida. Characteristic Bisimu- lation for Higher-Order Session Processes.Acta Informatica, 54:271–341, 2017

2017
[28]

Globally governed session semantics

Dimitrios Kouzapas and Nobuko Yoshida. Globally governed session semantics. Logical Methods in Computer Science, 10, 2014

2014
[29]

Modelling environments in call- by-value programming languages.Information and Computation, 185(2):182–210, 2003

Paul Blain Levy, John Power, and Hayo Thielecke. Modelling environments in call- by-value programming languages.Information and Computation, 185(2):182–210, 2003

2003
[30]

Non-linear communication via graded modal session types.Information and Computation, 301:105234, 2024

Danielle Marshall and Dominic Orchard. Non-linear communication via graded modal session types.Information and Computation, 301:105234, 2024

2024
[31]

Parametric monads and enriched adjunctions

Paul-André Melliès. Parametric monads and enriched adjunctions. Manuscript, 2012

2012
[32]

Quantitative programreasoningwithgradedmodaltypes.Proc

Dominic Orchard, Vilem-Benjamin Liepelt, and Harley Eades III. Quantitative programreasoningwithgradedmodaltypes.Proc. ACM Program. Lang.,3(ICFP), July 2019. Denotational reasoning for asynchronous multiparty session types 29

2019
[33]

Effects as sessions, sessions as effects

Dominic Orchard and Nobuko Yoshida. Effects as sessions, sessions as effects. In POPL 2016. ACM, 2016

2016
[34]

Adequacy for algebraic effects

Gordon Plotkin and John Power. Adequacy for algebraic effects. InInternational Conference on Foundations of Software Science and Computation Structures, pages 1–24. Springer, 2001

2001
[35]

Handlers of algebraic effects

Gordon Plotkin and Matija Pretnar. Handlers of algebraic effects. InEuropean Symposium on Programming, pages 80–94. Springer, 2009

2009
[36]

Concurrent monads for shared state

Exequiel Rivas and Tarmo Uustalu. Concurrent monads for shared state. In Proceedings of the 26th International Symposium on Principles and Practice of Declarative Programming, pages 1–13, 2024

2024
[37]

Category-graded algebraic theories and effect handlers.Elec- tronic Notes in Theoretical Informatics and Computer Science, 1, 2023

Takahiro Sanada. Category-graded algebraic theories and effect handlers.Elec- tronic Notes in Theoretical Informatics and Computer Science, 1, 2023

2023
[38]

Less is more: Multiparty session types revis- ited.Proceedings of the ACM on Programming Languages, 3(POPL):1–29, January 2019

Alceste Scalas and Nobuko Yoshida. Less is more: Multiparty session types revis- ited.Proceedings of the ACM on Programming Languages, 3(POPL):1–29, January 2019

2019
[39]

A.L. Smirnov. Graded monads and rings of polynomials.J. Math. Sci., 151(3):3032–3051, 2008

2008
[40]

Higher-order processes, func- tions, and sessions: A monadic integration

Bernardo Toninho, Luis Caires, and Frank Pfenning. Higher-order processes, func- tions, and sessions: A monadic integration. In Matthias Felleisen and Philippa Gardner, editors,Programming Languages and Systems, pages 350–369. Springer Berlin Heidelberg, 2013

2013
[41]

Informa- tion Flow Control in Cyclic Process Networks

Bas van den Heuvel, Farzaneh Derakhshan, and Stephanie Balzer. Informa- tion Flow Control in Cyclic Process Networks. In Jonathan Aldrich and Guido Salvaneschi, editors,38th European Conference on Object-Oriented Programming (ECOOP 2024), volume 313 ofLeibniz International Proceedings in Informatics (LIPIcs), pages 40:1–40:30. Schloss Dagstuhl – Leibniz-Z...

2024
[42]

Propositions as sessions

Philip Wadler. Propositions as sessions. InProceedings of ICFP 2012, pages 273–

2012
[43]

Se- mantic logical relations for timed message-passing protocols.Proc

Yue Yao, Grant Iraci, Cheng-En Chuang, Stephanie Balzer, and Lukasz Ziarek. Se- mantic logical relations for timed message-passing protocols.Proc. ACM Program. Lang., 9(POPL), January 2025

2025
[44]

A very gentle introduction to multiparty session types

Nobuko Yoshida and Lorenzo Gheri. A very gentle introduction to multiparty session types. In Dang Van Hung and Meenakshi D´Souza, editors,Distributed Computing and Internet Technology, pages 73–93. Springer International Publish- ing, 2020. A Detailed proofs A.1 Proofs for Section 3 Before giving the proofs for this section, we slightly elaborate on our d...

2020
[45]

IfU(T) =p⊕ i∈I ℓi⟨bi⟩.T i, then for everyi∈I, there is someU i such that U p!ℓi⟨bi⟩ ,− − − − →Ui andT i RU i
[46]

IfU(T) =p& i∈I ℓi⟨bi⟩.T i, thenRecvs p(U)
[47]

IfU(U) =p⊕ i∈I ℓi⟨bi⟩.U i, thenSends p(T)
[48]

IfU(U) =p& i∈I ℓi⟨bi⟩.U i, then for everyi∈I, there is someT i such that T p?ℓi⟨bi⟩ ,− − − − − →Ti andT i RU i
[49]

For everyX∈Θ, we haveU(T) =Xif and only ifU(U) =X. Asynchronous subtyping<:Θ is, by definition, the largest asynchronous type pre- simulation, in the sense that it is an asynchronous type pre-simulation, and every other such asynchronous type simulation is contained in<:Θ. Thus, to show that T< :Θ Uholds for a specificTandU, it suffices to exhibit an asyn...
[50]

,Xn 7→V n]

IfU p!ℓ⟨b⟩ ,− − − →U′, thenT p!ℓ⟨b⟩ ,− − − →T′, whereT ′ =U ′[X1 7→V 1, . . . ,Xn 7→V n]
[51]

IfRecvs p(U), thenRecvs p(T)
[52]

,Xn 7→V n]

IfU p?ℓ⟨b⟩ ,− − − →U′, thenT p?ℓ⟨b⟩ ,− − − →T′, whereT ′ =U ′[X1 7→V 1, . . . ,Xn 7→V n]
[53]

Proof.Each of the proofs is a trivial induction

IfSends p(U), thenSends p(T). Proof.Each of the proofs is a trivial induction. Lemma 32.Letpbe a participant, and letV 1, . . . ,Vn be session types. LetU be a session type with free type variablesX1, . . . ,Xn, and defineU ′ =U[X 1 7→ V1, . . . ,Xn 7→V n]
[54]

would require, for instance, thatRecvsp(T)impliesRecvs p(U)(and indeed subtyping does satisfy this stronger condition – see Lemma 39)

IfRecvs p(U′), then either (a)Recvsp(Vk)for somek, or (b)Recvs p(U). would require, for instance, thatRecvsp(T)impliesRecvs p(U)(and indeed subtyping does satisfy this stronger condition – see Lemma 39). Denotational reasoning for asynchronous multiparty session types 31
[55]

Proof.We give the proof of (1); the proof of (2) is similar

IfSends p(U′), then either (a)Sendsp(Vk)for somek, or (b)Sends p(U). Proof.We give the proof of (1); the proof of (2) is similar. We proceed by induction on the structure ofU. –IfUis a type variable, then we have (a) trivially. –IfU=q⊕ j∈J ℓj⟨bj⟩.U j, then we do not haveRecvsp(U′); this is a contra- diction. –IfU=q& j∈J ℓj⟨bj⟩.U j, then we haveRecvsp(Uj[X...
[56]

IfU(U) =p& i∈I ℓi⟨bi⟩.U i, thenT< :Θ Uholds iff, for everyi∈I, there is someT i such thatT p?ℓi⟨bi⟩ ,− − − − − →Ti andT i <:Θ Ui
[57]

Proof.We give the proof of (1); the proof of (2) is similar

IfU(T) =p⊕ i∈I ℓi⟨bi⟩.T i, thenT< :Θ Uholds iff, for everyi∈I, there is someU i such thatU p!ℓi⟨bi⟩ ,− − − − →Ui andT i <:Θ Ui. Proof.We give the proof of (1); the proof of (2) is similar. The only if direction is trivial. For the if direction, note that item (3) in the definition of subtyping holds trivially, while (4) is by assumption. To establish the ...
[58]

,Xn 7→V n]

IfU≺p& i∈I ℓi⟨bi⟩.U i, thenT≺p& i∈I ℓi⟨bi⟩.T i, whereT i =U i[X1 7→ V1, . . . ,Xn 7→V n]
[59]

,Xn 7→V n]

IfU≺p⊕ i∈I ℓi⟨bi⟩.U i, thenT≺p⊕ i∈I ℓi⟨bi⟩.T i, whereT i =U i[X1 7→ V1, . . . ,Xn 7→V n]. Proof.Each of the proofs is a trivial induction. Lemma 36
[60]

Denotational reasoning for asynchronous multiparty session types 33

We haveRecvs p(U)iff there exist{(ℓ i,b i,U i)}i∈I such thatU≺p& i∈I ℓi⟨bi⟩.U i. Denotational reasoning for asynchronous multiparty session types 33
[61]

Proof.We give the proof of (1); the proof of (2) is similar

We haveSends p(T)iff there exist{(ℓ i,b i,T i)}i∈I such thatT≺p⊕ i∈I ℓi⟨bi⟩.T i. Proof.We give the proof of (1); the proof of (2) is similar. The if direction is an easy induction on the derivation of≺, using Lemma 33 for the recursive case. For the only if direction, we proceed by induction on Recvsp(U). Uhe only non-trivial case is[Recvs-rec]. In this c...
[62]

IfU(T) =p& i∈I ℓi⟨bi⟩.T i, then there existJ⊆Iand{U i}i∈J, such that U≺p& i∈J ℓi⟨bi⟩.U i, andT i <:Θ Ui for eachi∈J
[63]

Proof.We give the proof of (1); the proof of (2) is similar

IfU(U) =p⊕ i∈I ℓi⟨bi⟩.U i, then there existJ⊆Iand{T i}i∈J, such that T≺p⊕ i∈J ℓi⟨bi⟩.T i, andT i <:Θ Ui for eachi∈J. Proof.We give the proof of (1); the proof of (2) is similar. We haveRecvsp(U) becauseT< :Θ U, and henceU≺p& k∈K ℓ′ k⟨b′ k⟩.U ′ k by Lemma 36. We proceed by induction on the latter. –If the proof is by rule[≺&-base], thenU=p& k∈K ℓ′ k⟨b′ k⟩....
[64]

IfIis a non-empty finite set, then there existU i such thatU≺p& i∈I ℓi⟨bi⟩.U i andU i q!ℓ′⟨b′⟩ ,− − − − →U′ i for alli∈I, exactly when there exists someU ′ such thatU q!ℓ′⟨b′⟩ ,− − − − →U′ ≺p& i∈I ℓi⟨bi⟩.U ′ i. 34 D. McDermott and N. Yoshida
[65]

Ifp̸=q,U≺p& i∈I ℓi⟨bi⟩.U i andU i ≺q& j∈Ji ℓ′ j⟨b′ j⟩.U ij, then there existU ′ j such thatU≺q& j∈J ℓ′ j⟨b′ j⟩.U ′ j andU ′ j ≺p& i∈Ij ℓi⟨bi⟩.U ij, where Ij ={i∈I|j∈J i}andJ=∪ i∈I Ji
[66]

IfT p!ℓ⟨b⟩ ,− − − →UandT q?ℓ′⟨b′⟩ ,− − − − →T′, then there is someU′ such thatT ′ p!ℓ⟨b⟩ ,− − − →U′ andU q?ℓ′⟨b′⟩ ,− − − − →U′
[67]

Ifp̸=q,Iis a non-empty finite set, andU p?ℓi⟨bi⟩ ,− − − − − →Ui q?ℓ′⟨b′⟩ ,− − − − →U′ i for each i∈I, then there is someU ′ such thatU q?ℓ′⟨b′⟩ ,− − − − →U′ p?ℓi⟨bi⟩ ,− − − − − →U′ i for each i∈I
[68]

IfIis a non-empty finite set, then there existU i such thatU≺p⊕ i∈I ℓi⟨bi⟩.U i andU i q?ℓ′⟨b′⟩ ,− − − − →U′ i for alli∈I, exactly when there exists someU ′ such thatU q?ℓ′⟨b′⟩ ,− − − − →U′ ≺p⊕ i∈I ℓi⟨bi⟩.U ′ i
[69]

Proof.For (1), sinceIis finite, there is some natural numberhsuch that for everyi, the derivation ofU p!ℓi⟨bi⟩ ,− − − − →Ui has height at mosth

Ifp̸=q,U≺p⊕ i∈I ℓi⟨bi⟩.U i andU i ≺q⊕ j∈Ji ℓ′ j⟨b′ j⟩.U ij, then there existU ′ j such thatU≺q⊕ j∈J ℓ′ j⟨b′ j⟩.U ′ j andU ′ j ≺p⊕ i∈Ij ℓi⟨bi⟩.U ij, where Ij ={i∈I|j∈J i}andJ=∪ i∈I Ji. Proof.For (1), sinceIis finite, there is some natural numberhsuch that for everyi, the derivation ofU p!ℓi⟨bi⟩ ,− − − − →Ui has height at mosth. We proceed by induction onh....
[70]

IfT p!ℓ⟨b⟩ ,− − − →T′, then there is someU′ such thatU p!ℓ⟨b⟩ ,− − − →U′ andT ′ <:Θ U′
[71]

IfT≺p& i∈I ℓi⟨bi⟩.T i, then there existUi such thatU≺p& i∈I ℓi⟨bi⟩.U i andT i <:Θ Ui
[72]

IfRecvs p(T)thenRecvs p(U)
[73]

IfU p?ℓ⟨b⟩ ,− − − →U′, then there is someT′ such thatT p?ℓ⟨b⟩ ,− − − →T′ andT ′ <:Θ U′
[74]

IfU≺p⊕ i∈I ℓi⟨bi⟩.U i, then there existTi such thatT≺p⊕ i∈I ℓi⟨bi⟩.T i andT i <:Θ Ui
[75]

Proof.We give the proofs of (1), (2), and (3); the proofs of (4), (5) and (6) are similar

IfSends p(U)thenSends p(T). Proof.We give the proofs of (1), (2), and (3); the proofs of (4), (5) and (6) are similar. The proof of (1) is by induction onT p!ℓ⟨b⟩ ,− − − →T′. The base case is an imme- diate consequence ofT< :Θ U. For[ ! ,− →-⊕], the result follows from the inductive hypothesis and Lemma 38(1). For[ ! ,− →-&], the result follows from Lemma...
[76]

IfSends p(T), thenSends p(T·T ′)
[77]

IfT p?ℓ⟨b⟩ ,− − − →UthenT·T′ p?ℓ⟨b⟩ ,− − − →U·T′
[78]

Proof.Each of these is a trivial induction

IfRecvs p(T), thenRecvs p(T·T ′). Proof.Each of these is a trivial induction. Lemma 41.1. IfT·T ′ p!ℓ⟨b⟩ ,− − − →UandSendsp(T), thenU=U ′ ·T ′, for someU′ such thatU p!ℓ⟨b⟩ ,− − − →U′
[79]

Proof.The proof of (1) is by induction on the derivation ofT·T′ p!ℓ⟨b⟩ ,− − − →U

IfT·T ′ p?ℓ⟨b⟩ ,− − − →UandRecvsp(T), thenU=U ′ ·T ′, for someU ′ such that U p?ℓ⟨b⟩ ,− − − →U′. Proof.The proof of (1) is by induction on the derivation ofT·T′ p!ℓ⟨b⟩ ,− − − →U. For rule[ ! ,− →-base],Sendsp(T)tells us thatTis notend, and hence thatTis an inter- nal choice onp, and the result follows immediately. For rule[ ! ,− →-⊕],Sendsp(T) can only be...
[80]

IfΘ#Φ#Γ⊢ returnv:b#UthenΓ⊢ v v:bandend< :Θ h

Showing first 80 references.