Pith. sign in

REVIEW 4 minor 116 references

Global types and event structure semantics for asynchronous multiparty sessions

T0 review · 0 major / 4 minor · reviewed 2026-05-24 · grok-4.3

Challenge this review Download PDF Read on arXiv ↗ Review JSON

Pith's one-line read The event structure of a typable asynchronous multiparty session equals the event structure of its global type.

desk verdict The paper defines new more permissive global types for async multiparty sessions, interprets them as prime event structures, and proves equivalence to the flow event structure semantics of typable sessions. read the letter →

arxiv 2102.00865 v8 submitted 2021-02-01 cs.LO

Ilaria Castellani (INDES , Inria , UCA) , Mariangiola Dezani-Ciancaglini (UNITO) , Paola Giannini (UPO) This is my paper · ORCID
classification cs.LO
keywords globaltypeseventstructuresasynchronouscommunicationmultipartysessionssessionsemanticsprogress
verification ladder T0 review T1 audit T2 compute T3 formal

The pith

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

The reading

The paper shows that when a session is typable under newly defined global types, its Flow Event Structure semantics is equivalent to the Prime Event Structure semantics of the corresponding global type. These global types are designed to reflect asynchrony directly and are more permissive than prior versions while still guaranteeing progress and other standard session properties. A reader would care because the result supplies a precise semantic link between syntactic types and behavioral models for concurrent message-passing programs. The work therefore gives a foundation for reasoning about asynchronous sessions via event structures rather than through operational rules alone. The equivalence is proved by showing that both interpretations produce the same causal and conflict relations on events.

What carries the argument

Equivalence between the Flow Event Structure of a typable session and the Prime Event Structure of its global type.

What would settle it

A concrete session that is typable under the new global types yet produces a Flow Event Structure whose causal or conflict relations differ from those of the Prime Event Structure of its global type.

Watch

Extended reading notes

Core claim

We propose an interpretation of multiparty sessions with asynchronous communication as Flow Event Structures. We introduce a new notion of global type for asynchronous multiparty sessions, ensuring the expected properties for sessions, including progress. Our global types, which reflect asynchrony more directly than standard global types and are more permissive, are themselves interpreted as Prime Event Structures. The main result is that the Event Structure interpretation of a session is equivalent, when the session is typable, to the Event Structure interpretation of its global type.

Load-bearing premise

The new global types must capture asynchronous communication directly while still enforcing progress and other session properties.

Editorial extensions

If this is right

  • Typable sessions inherit the causal ordering and conflict information encoded in their global types.
  • Progress and safety properties proved on the global type carry over to the session implementation.
  • Asynchronous message ordering is represented explicitly in the event structures without additional synchronization assumptions.
  • More permissive global types can still be used for verification because the equivalence preserves the intended behavior.

Reading between the lines

Editorial extensions of the paper, not claims the author makes directly.

  • The result opens the possibility of using event-structure tools directly on global types to check properties of running sessions.
  • Similar equivalences might be investigated for other communication models such as broadcast or unreliable channels.
  • One could test the equivalence by generating small typable sessions and comparing their event structures by hand or with automated tools.
Share X Bluesky LinkedIn Reddit HN

Signed reviews

No signed human review yet.

Request a human review

A listed scientist reviews the paper for a fee and the review publishes here regardless of verdict. See the reviewers or get listed.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit.

Referee Report

0 major / 4 minor

Summary. The paper interprets asynchronous multiparty sessions as Flow Event Structures and introduces new global types (more permissive and directly reflecting asynchrony) interpreted as Prime Event Structures. The central claim is an equivalence between the session's Flow ES semantics and the global type's Prime ES semantics whenever the session is typable under the new types; the types are shown to ensure progress and standard session properties.

Significance. If the equivalence holds, the work supplies a semantic bridge between session calculi and event structures that supports compositional reasoning about asynchrony and concurrency. The permissiveness of the new global types while preserving safety properties is a concrete advance over standard global types; the formal equivalence result itself is a strength when accompanied by the definitions and proofs in the manuscript.

minor comments (4)
  1. §4.2: the inductive definition of the new global type constructors would benefit from an explicit side-by-side comparison table with the standard global types of Honda et al. to make the increased permissiveness concrete.
  2. §5, Definition 5.3: the mapping from session processes to Flow Event Structures uses an auxiliary relation whose well-definedness is stated but whose proof is only sketched; a short lemma stating the conditions under which the relation is a partial function would improve readability.
  3. Figure 3: the event-structure diagram is missing node labels corresponding to the actions in the running example, making it difficult to verify the claimed equivalence by inspection.
  4. §6: the statement of the main theorem (equivalence) refers to 'typable sessions' without recalling the precise typing judgment; a forward reference to the typing rules in §3 would help.

Simulated Author's Rebuttal

0 responses · 0 unresolved

We thank the referee for the positive assessment of our manuscript, the accurate summary of its contributions, and the recommendation of minor revision. No specific major comments were raised in the report.

Circularity Check

0 steps flagged · score 0.0 of 10

No significant circularity

full rationale

The paper defines new global types for asynchronous sessions and provides two separate Event Structure interpretations (Flow ES for sessions, Prime ES for global types), then proves an equivalence theorem for typable sessions. No step reduces a claimed prediction or first-principles result to a fitted parameter, self-definition, or load-bearing self-citation; the equivalence is presented as an independent semantic result to be established from the definitions. The construction is self-contained against external benchmarks of session calculi and event structures.

Assumptions & free parameters 0 free parameters · 1 assumptions · 0 invented entities

Based on abstract, the work relies on standard mathematical structures from concurrency theory with no free parameters, invented entities, or ad-hoc axioms mentioned.

assumptions (1)
  • standard math Standard definitions and properties of Flow Event Structures and Prime Event Structures
    The interpretations build directly on established event structure models in the literature.

how reviews work

0 comments
Cite this review

Pith. "Pith review of Global types and event structure semantics for asynchronous multiparty sessions." pith.science (2026). https://pith.science/paper/2102.00865

@misc{pith2026210200865,
  author       = {Pith},
  title        = {Pith review of: Global types and event structure semantics for asynchronous multiparty sessions},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/2102.00865}},
  note         = {Machine review of arXiv:2102.00865}
}
read the original abstract

We propose an interpretation of multiparty sessions with asynchronous communication as Flow Event Structures. We introduce a new notion of global type for asynchronous multiparty sessions, ensuring the expected properties for sessions, including progress. Our global types, which reflect asynchrony more directly than standard global types and are more permissive, are themselves interpreted as Prime Event Structures. The main result is that the Event Structure interpretation of a session is equivalent, when the session is typable, to the Event Structure interpretation of its global type.

Figures

Figures reproduced from arXiv: 2102.00865 by the authors.

Figure 1
Figure 1. LTS for networks. p to q and the exclamation/question mark as the mode (write/read) in which the channel is used. The LTS semantics of networks, defined modulo ≡, is specified by the two Rules [SEND] and [RCV] given in [PITH_FULL_IMAGE:figures/full_fig_p006_1.png] view at source ↗
Figure 2
Figure 2. Projection of global types onto participants. [PITH_FULL_IMAGE:figures/full_fig_p008_2.png] view at source ↗
Figure 3
Figure 3. Balancing predicate. We show now that the definition of projection given in [PITH_FULL_IMAGE:figures/full_fig_p010_3.png] view at source ↗
Figures from the paper (5 more)
Figure 4
Figure 4. Figure 4: Preorder on processes and network typing rule. [PITH_FULL_IMAGE:figures/full_fig_p012_4.png]
Figure 5
Figure 5. Figure 5: LTS for asynchronous types. since each participant only needs to do the output before the input. Notice that this network cannot be typed with the standard global types of [4]. The network p[[r!ℓ ]] k q[[ p?ℓ1 + p?ℓ2 ]] k r[[ p?ℓ ]] k hp, ℓ1, qi can be typed by the asy…
Figure 3
Figure 3. Figure 3: Then G k M qp?ℓ −−−→ G ′ k M′ by Rule [EXT-IN] of [PITH_FULL_IMAGE:figures/full_fig_p016_3.png]
Figure 5
Figure 5. Figure 5: Case id > 1. As in the proof of Statement (1), by applying Rule [EXT-OUT] or Rule [EXT-IN] of [PITH_FULL_IMAGE:figures/full_fig_p017_5.png]
Figure 6
Figure 6. Figure 6: (a) FES of N k ∅ in Example 6.13. (b) PES of G k ∅ in Example 7.18 [PITH_FULL_IMAGE:figures/full_fig_p034_6.png]

Discussion (0). Continue with ORCID to comment.

Reference graph

Works this paper leans on

116 extracted references · 116 canonical work pages

  1. [1]

    An interaction-based langua ge and its typing system

    Takeuchi K, Honda K, Kubo M. An interaction-based langua ge and its typing system. In: Hankin C (ed.), P ARLE, volume 817 of LNCS. Springer, 1994 pp. 122–138. doi:10.1007/ BFb0053567

    work page 1994

  2. [2]

    In: Proceedings of the 7th European Symposium on Pro- gramming (ESOP 1998), Springer, pp

    Honda K, V asconcelos VT, Kubo M. Language primitives and type discipline for structured communication-based programming. In: Hankin C (ed.), ESOP , volume 1381 of LNCS. Springer, 1998 pp. 122–138. doi:10.1007/BFb0053567

    work page doi:10.1007/bfb0053567 1998

  3. [3]

    Multiparty asynchronous s ession types

    Honda K, Y oshida N, Carbone M. Multiparty asynchronous s ession types. In: Necula GC, Wadler P (eds.), POPL. ACM Press, 2008 pp. 273–284. doi:10.1 145/1328897.1328472

    work page arXiv 2008

  4. [4]

    Multiparty asynchronous s ession types

    Honda K, Y oshida N, Carbone M. Multiparty asynchronous s ession types. Journal of ACM,

    work page

  5. [5]

    In: Pro- ceedings of the 35th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL 2008), ACM, pp

    63(1):9:1–9:67. doi:10.1145/2827695

    work page doi:10.1145/2827695

  6. [6]

    Behavioral types in p rogramming languages

    Ancona D, Bono V , Bravetti M, Campos J, Castagna G, Deni´ e lou P , Gay SJ, Gesbert N, Giachino E, Hu R, Johnsen EB, Martins F, Mascardi V , Montesi F , Neykova R, Ng N, Padovani L, V asconcelos VT, Y oshida N. Behavioral types in p rogramming languages. F oundations and Trends in Programming Languages , 2016. 3(2-3):95–230. doi:10.1561/ 2500000031

    work page 2016

  7. [7]

    Multiparty session types meet co mmunicating automata

    Deni´ elou P , Y oshida N. Multiparty session types meet co mmunicating automata. In: Seidl H (ed.), ESOP , volume 7211 of LNCS. Springer, 2012 pp. 194–213. doi:10.1007/ 978-3-642-28869-2 \ 10

    work page 2012

  8. [8]

    doi:10.1145/2676726.2676969 Pierre Letouzey

    Lange J, Tuosto E, Y oshida N. From communicating machine s to graphical choreographies. In: Rajamani SK, Walker D (eds.), POPL. ACM Press, 2015 pp. 22 1–232. doi:10.1145/ 2676726.2676964

    work page arXiv 2015

Show all 116 references
  1. [9]

    Semantics of global view of choreo graphies

    Tuosto E, Guanciale R. Semantics of global view of choreo graphies. Journal of Logic and Algebraic Methods in Programming, 2018. 95:17–40. doi:10.1016/j.jlamp.2017.11.002

    2018 doi

  2. [10]

    Session types as intuitionistic li near propositions

    Caires L, Pfenning F. Session types as intuitionistic li near propositions. In: Gastin P , Laroussinie F (eds.), CONCUR, volume 6269 of LNCS. Springer, 2010 pp. 222–236. doi: 10.1007/978-3-642-15375-4 \ 16

    2010 doi

  3. [11]

    Dependent session type s via intuitionistic linear type theory

    Toninho B, Caires L, Pfenning F. Dependent session type s via intuitionistic linear type theory. In: Schneider-Kamp P , Hanus M (eds.), PPDP . ACM Pres s, 2011 pp. 161–172. doi:10.1145/2003476.2003499

    2011 doi

  4. [12]

    Propositions as sessions

    Wadler P . Propositions as sessions. Journal of Functional Programming , 2014. 24(2- 3):384–418. doi:10.1017/S095679681400001X

    2014 doi

  5. [13]

    Linear logical relations and observational equiv- alences for session-based concurrency

    P´ erez JA, Caires L, Pfenning F, Toninho B. Linear logical relations and observational equiv- alences for session-based concurrency. Information and Computation , 2014. 239:254–302. doi:10.1016/j.ic.2014.08.001

    2014 doi

  6. [14]

    Linear logic propositi ons as session types

    Caires L, Pfenning F, Toninho B. Linear logic propositi ons as session types. Mathematical Structures in Computer Science , 2016. 26(3):367–423. doi:10.1017/S0960129514000218

    2016 doi

  7. [15]

    Event structure semantics for multiparty sessions

    Castellani I, Dezani-Ciancaglini M, Giannini P . Event structure semantics for multiparty sessions. CoRR, 2022. abs/2201.00221. 2201.00221

    2022

  8. [16]

    An introduction to event structures

    Winskel G. An introduction to event structures. In: de B akker JW , de Roever WP , Rozenberg G (eds.), REX: Linear Time, Branching Time and Partial Order in Logics and Models for Concurrency, volume 354 of LNCS. Springer, 1988 pp. 364–397. 50 I.Castellani, M.Dezani, P .Giannin...

    1988

  9. [17]

    Precise subtyping for synchronous multiparty sessions

    Dezani-Ciancaglini M, Ghilezan S, Jaksic S, Pantovic J , Y oshida N. Precise subtyping for synchronous multiparty sessions. In: Gay S, Alglave J (eds. ), PLACES, volume 203 of EPTCS. Open Publishing Association, 2015 pp. 29 – 44. doi:10.4204 /EPTCS.203.3

    2015

  10. [18]

    Permutation of transitions: an event structure semantics for CCS and SCCS

    Boudol G, Castellani I. Permutation of transitions: an event structure semantics for CCS and SCCS. In: de Bakker JW , de Roever WP , Rozenberg G (eds.), R EX: Linear Time, Branching Time and Partial Order in Logics and Models for Con currency, volume 354 of LNCS. Springer, 198...

    1988 doi

  11. [19]

    Flow models of distributed comp utations: three equivalent semantics for CCS

    Boudol G, Castellani I. Flow models of distributed comp utations: three equivalent semantics for CCS. Information and Computation , 1994. 114(2):247–314. doi:10.1006/inco.1994. 1088

    1994 doi

  12. [20]

    Events in computation

    Winskel G. Events in computation. Ph.D. thesis, Univer sity of Edinburgh, 1980

    1980

  13. [21]

    Petri nets, event struc tures and domains, part I

    Nielsen M, Plotkin G, Winskel G. Petri nets, event struc tures and domains, part I. Theoret- ical Computer Science , 1981. 13(1):85–108. doi:10.1016/0304-3975(81)90112-2

    1981 doi

  14. [22]

    Global principal typing in partially commutative asyn- chronous sessions

    Mostrous D, Y oshida N, Honda K. Global principal typing in partially commutative asyn- chronous sessions. In: Castagna G (ed.), ESOP , volume 5502 o f LNCS. Springer, 2009 pp. 316–332. doi:10.1007/978-3-642-00590-9 \ 23

    2009 doi

  15. [23]

    Undecidability of a synchronous session subtyping

    Bravetti M, Carbone M, Zavattaro G. Undecidability of a synchronous session subtyping. Information and Computation , 2017. 256:300–320. doi:10.1016/j.ic.2017.07.010

    2017 doi

  16. [24]

    On the undecidability of asynchrono us session subtyping

    Lange J, Y oshida N. On the undecidability of asynchrono us session subtyping. In: Esparza J, Murawski AS (eds.), FOSSACS, volume 10203 of LNCS. 2017 pp. 441–457. doi:10. 1007/978-3-662-54458-7 \ 26

    2017

  17. [25]

    Fundamental properties of infinite trees

    Courcelle B. Fundamental properties of infinite trees. Theoretical Computer Science, 1983. 25:95–169. doi:10.1016/0304-3975(83)90059-2

    1983 doi

  18. [26]

    Less is more: multiparty session ty pes revisited

    Scalas A, Y oshida N. Less is more: multiparty session ty pes revisited. Proc. ACM Program. Lang., 2019. 3(POPL):30:1–30:29. doi:10.1145/3290343

    2019 doi

  19. [27]

    Deconfine d global types for asynchronous sessions

    Dagnino F, Giannini P , Dezani-Ciancaglini M. Deconfine d global types for asynchronous sessions. CoRR, 2021. abs/2111.11984. 2111.11984

    2021

  20. [28]

    Types and Programming Languages

    Pierce BC. Types and Programming Languages. MIT Press, 2002. ISBN 978-0-262-16209- 8

    2002

  21. [29]

    Dynamic multirole session typ es

    Deni´ elou PM, Y oshida N. Dynamic multirole session typ es. In: Thomas Ball MS (ed.), POPL. ACM Press, 2011 pp. 435–446. doi:10.1145/1926385.19 26435

    2011 doi

  22. [30]

    G lobal progress for dynami- cally interleaved multiparty sessions

    Coppo M, Dezani-Ciancaglini M, Y oshida N, Padovani L. G lobal progress for dynami- cally interleaved multiparty sessions. Mathematical Structures in Computer Science , 2016. 26(2):238–302. doi:10.1017/S0960129514000188

    2016 doi

  23. [31]

    Subtyping for session types in the pi calcu lus

    Gay S, Hole M. Subtyping for session types in the pi calcu lus. Acta Informatica , 2005. 42(2/3):191–225. doi:10.1007/s00236-005-0177-z

    2005 doi

  24. [32]

    Full abstraction in a subtyped pi- calculus with linear types

    Demangeon R, Honda K. Full abstraction in a subtyped pi- calculus with linear types. In: Katoen J, K¨ onig B (eds.), CONCUR, volume 6901 of LNCS. Springer, 2011 pp. 280–296. doi:10.1007/978-3-642-23217-6 \ 19

    2011 doi

  25. [33]

    Subtyping supports safe session substitution

    Gay S. Subtyping supports safe session substitution. I n: Lindley S, McBride C, Trinder PW , Sannella D (eds.), A List of Successes That Can Change the Wor ld - Essays Dedicated to Philip Wadler on the Occasion of His 60th Birthday, volume 96 00 of LNCS. Springer, 2016 pp. 95–...

    2016 doi

  26. [34]

    Composition and decomposition of multiparty sessions

    Barbanera F, Dezani-Ciancaglini M, Lanese I, Tuosto E. Composition and decomposition of multiparty sessions. Journal of Logic and Algebraic Methods Program., 2021. 119:100620. doi:10.1016/j.jlamp.2020.100620

    2021 doi

  27. [35]

    Found ations of session types and behavioural contracts

    H¨ uttel H, Lanese I, V asconcelos VT, Caires L, Carbone M , Deni´ elou PM, Mostrous D, Padovani L, Ravara A, Tuosto E, Vieira HT, Zavattaro G. Found ations of session types and behavioural contracts. ACM Computing Surveys , 2016. 49(1):3:1–3:36. doi:10.1145/ 2873052

    2016

  28. [36]

    Flow models of distributed comp utations: event structures and nets

    Boudol G, Castellani I. Flow models of distributed comp utations: event structures and nets. Research Report 1482, INRIA, 1991

    1991

  29. [37]

    Event Structure Semantics for Multiparty Sessions

    Castellani I, Dezani-Ciancaglini M, Giannini P . Event Structure Semantics for Multiparty Sessions. In: Boreale M, Corradini F, Loreti M, Pugliese R (e ds.), Models, Languages, and Tools for Concurrent and Distributed Programming - Essays D edicated to Rocco De Nicola on the O...

    2019 doi

  30. [38]

    The polyadic pi-calculus (Abstract)

    Milner R. The polyadic pi-calculus (Abstract). In: Cle aveland R (ed.), CONCUR, volume 630 of LNCS. Springer, 1992 p. 1. doi:10.1007/BFb0084778

    1992 doi

  31. [39]

    Typing and subtyping for mobile processes

    Pierce BC, Sangiorgi D. Typing and subtyping for mobile processes. Mathematical Struc- tures in Computer Science , 1996. 6(5):376–385. doi:10.1017/S096012950007002X

    1996 doi

  32. [40]

    Type-based information flow analysis for t he pi-calculus

    Kobayashi N. Type-based information flow analysis for t he pi-calculus. Acta Informatica,

  33. [41]

    doi:10.1007/s00236-005-0179-x

    42(4-5):291–347. doi:10.1007/s00236-005-0179-x

    doi

  34. [42]

    A type system for lock-free processes

    Kobayashi N. A type system for lock-free processes. Information and Computation , 2002. 177(2):122–159. doi:10.1016/S0890-5401(02)93171-8

    2002 doi

  35. [43]

    A new type system for deadlock-free proces ses

    Kobayashi N. A new type system for deadlock-free proces ses. In: Baier C, Hermanns H (eds.), CONCUR, volume 4137 of LNCS. Springer, 2006 pp. 233–247. doi:10.1007/ 11817949\ 16

    2006

  36. [44]

    Session types revisi ted

    Dardha O, Giachino E, Sangiorgi D. Session types revisi ted. In: Schreye DD, Janssens G, King A (eds.), PPDP . ACM, 2012 pp. 139–150. doi:10.1145/237 0776.2370794

    2012 doi

  37. [45]

    Type reconstruction for the linear π -calculus with composite regular types

    Padovani L. Type reconstruction for the linear π -calculus with composite regular types. Logical Methods in Computer Science , 2015. 11(4). doi:10.2168/LMCS-11(4:13)2015

    2015 doi

  38. [46]

    Observational equiva lence for multiparty sessions

    Severi P , Dezani-Ciancaglini M. Observational equiva lence for multiparty sessions. Funda- menta Informaticae, 2019. 167:267–305. doi:10.3233/FI-2019-1863

    2019 doi

  39. [47]

    On the boundary betw een decidability and undecid- ability of asynchronous session subtyping

    Bravetti M, Carbone M, Zavattaro G. On the boundary betw een decidability and undecid- ability of asynchronous session subtyping. Theoretical Computer Science, 2018. 722:19–51. doi:10.1016/j.tcs.2018.02.010

    2018 doi

  40. [48]

    A sound algorithm for asyn- chronous session subtyping and its implementation

    Bravetti M, Carbone M, Lange J, Y oshida N, Zavattaro G. A sound algorithm for asyn- chronous session subtyping and its implementation. Logical Methods in Computer Science ,

  41. [49]

    doi:10.23638/LMCS-17(1:20)2021

    17(1). doi:10.23638/LMCS-17(1:20)2021

    2021 doi

  42. [50]

    Precise subtyping for asyn- chronous multiparty sessions

    Ghilezan S, Pantovi´ c J, Proki´ c I, Scalas A, Y oshida N. Precise subtyping for asyn- chronous multiparty sessions. Proc. ACM Program. Lang. , 2021. 5(POPL):1–28. doi: 10.1145/3434297

    2021 doi

  43. [51]

    Event structure semantics for CCS and relate d languages

    Winskel G. Event structure semantics for CCS and relate d languages. In: Nielsen M, Schmidt EM (eds.), ICALP, volume 140 of LNCS. Springer, 1982 pp. 561–576. doi:10. 1007/BFb0012800. 52 I.Castellani, M.Dezani, P .Giannini/ Types and Semantics for Asynchronous Sessions

    1982

  44. [52]

    On the semantics of concurrency : partial orders and transition systems

    Boudol G, Castellani I. On the semantics of concurrency : partial orders and transition systems. In: Ehrig H, Kowalski RA, Levi G, Montanari U (eds.) , TAPSOFT, volume 249 of LNCS. Springer, 1987 pp. 123–137. doi:10.1007/3-540-17660-8 \ 52

    1987 doi

  45. [53]

    On the consistency of truly concurrent operational and denotational semantics

    Degano P , De Nicola R, Montanari U. On the consistency of truly concurrent operational and denotational semantics. In: Chandra AK (ed.), LICS. IEE E Computer Society Press Press, 1988 pp. 133–141. doi:10.1109/LICS.1988.5112

    1988 doi

  46. [54]

    A partial ordering se mantics for CCS

    Degano P , De Nicola R, Montanari U. A partial ordering se mantics for CCS. Theoretical Computer Science, 1990. 75(3):223–262. doi:10.1016/0304-3975(90)90095-Y

    1990 doi

  47. [56]

    A theory of communicatin g sequential processes

    Brookes S, Hoare CA, Roscoe AW . A theory of communicatin g sequential processes. Jour- nal of ACM, 1984. 31(3):560–599. doi:10.1145/828.833

    1984 doi

  48. [57]

    TCSP: theory of communicating sequential pr ocesses

    Olderog E. TCSP: theory of communicating sequential pr ocesses. In: Brauer W , Reisig W , Rozenberg G (eds.), Advances in Petri Nets, volume 255 of LNCS. Springer, 1986 pp. 441–465. doi:10.1007/3-540-17906-2 \ 34

    1986 doi

  49. [58]

    Modelling nondeterministic concurr ent processes with event structures

    Loogen R, Goltz U. Modelling nondeterministic concurr ent processes with event structures. Fundamenta Informaticae, 1991. 14(1):39–74. doi:10.3233/FI-1991-14103

    1991 doi

  50. [59]

    The connection between an event structure semantics and an operational semantics for TCSP

    Baier C, Majster-Cederbaum ME. The connection between an event structure semantics and an operational semantics for TCSP. Acta Informatica , 1994. 31(1):81–104. doi:10.1007/ BF01178923

    1994

  51. [60]

    Bundle event structures: a non-interleavi ng semantics for LOTOS

    Langerak R. Bundle event structures: a non-interleavi ng semantics for LOTOS. In: Diaz M, Groz R (eds.), FORTE. North-Holland. ISBN 0-444-89282-6 , 1993 pp. 331–346

    1993

  52. [61]

    Quantitative and qualitative extensions of e vent structures

    Katoen J. Quantitative and qualitative extensions of e vent structures. Ph.D. thesis, Univer- sity of Twente, 1996

    1996

  53. [62]

    Compositional event stru cture semantics for the internal π - Calculus

    Crafa S, V aracca D, Y oshida N. Compositional event stru cture semantics for the internal π - Calculus. In: Caires L, V asconcelos VT (eds.), CONCUR, volume 4703 of LNCS. Springer, 2007 pp. 317–332. doi:10.1007/978-3-540-74407-8 \ 22

    2007 doi

  54. [63]

    Typed event structures and the lin ear π -calculus

    V aracca D, Y oshida N. Typed event structures and the lin ear π -calculus. Theoretical Com- puter Science, 2010. 411(19):1949–1973. doi:10.1016/j.tcs.2010.01.024

    2010 doi

  55. [64]

    Event structure semantic s of parallel extrusion in the π - calculus

    Crafa S, V aracca D, Y oshida N. Event structure semantic s of parallel extrusion in the π - calculus. In: Birkedal L (ed.), FOSSACS, volume 7213 of LNCS. Springer, 2012 pp. 225–

    2012

  56. [65]

    doi:10.1007/978-3-642-28729-9 \ 15

    doi

  57. [66]

    Operational and denotational semantics f or the reversible π -calculus

    Cristescu I. Operational and denotational semantics f or the reversible π -calculus. Ph.D. thesis, University Paris Diderot - Paris 7, 2015

    2015

  58. [67]

    Rigid families for CCS and the π -calculus

    Cristescu I, Krivine J, V aracca D. Rigid families for CCS and the π -calculus. In: Leucker M, Rueda C, V alencia FD (eds.), ICTAC, volume 9399 of LNCS. Springer, 2015 pp. 223–240. doi:10.1007/978-3-319-25150-9 \ 14

    2015 doi

  59. [68]

    Rigid families for th e reversible π -calculus

    Cristescu I, Krivine J, V aracca D. Rigid families for th e reversible π -calculus. In: Devitt SJ, Lanese I (eds.), Reversible Computation, volume 9720 of LNCS. Springer, 2016 pp. 3–19. doi:10.1007/978-3-319-40578-0 \ 1

    2016 doi

  60. [69]

    Towards refinable choreographies

    de’ Liguoro U, Melgratti HC, Tuosto E. Towards refinable choreographies. In: Lange J, Mavridou A, Safina L, Scalas A (eds.), ICE, volume 324 of EPTCS. Open Publishing Association, 2020 pp. 61–77. doi:10.4204/EPTCS.324.6. I.Castellani, M.Dezani, P .Giannini/ Types and Semantics f...

    2020 doi

  61. [70]

    Concurrent strategies

    Rideau S, Winskel G. Concurrent strategies. In: Grohe M (ed.), LICS. IEEE Computer Society, 2011 pp. 409–418. doi:10.1109/LICS.2011.13

    2011 doi

  62. [71]

    A truly concurrent game model of t he asynchronous π -calculus

    Sakayori K, Tsukada T. A truly concurrent game model of t he asynchronous π -calculus. In: Esparza J, Murawski AS (eds.), FOSSACS, volume 10203 of LNCS. 2017 pp. 389–406. doi:10.1007/978-3-662-54458-7 \ 23

    2017 doi

  63. [72]

    Towards reversible sessions

    Tiezzi F, Y oshida N. Towards reversible sessions. In: D onaldson AF, V asconcelos VT (eds.), PLACES, volume 155 of EPTCS. Open Publishing Association, 2014 pp. 17–24. doi:10.4204/EPTCS.155.3

    2014 doi

  64. [73]

    Reversing single sessions

    Tiezzi F, Y oshida N. Reversing single sessions. In: Dev itt SJ, Lanese I (eds.), RC, volume 9720 of LNCS. Springer, 2016 pp. 52–69. doi:10.1007/978-3-319-40578- 0\ 4

    2016 doi

  65. [74]

    Causally consistent reversible choreographies: a monitors-as- memories approach

    Mezzina CA, P´ erez JA. Causally consistent reversible choreographies: a monitors-as- memories approach. In: V anhoof W , Pientka B (eds.), PPDP . ACM Press, 2017 pp. 127–138. doi:10.1145/3131851.3131864

    2017 doi

  66. [75]

    Reversibility in session-basedconcurrency: A fresh look

    Mezzina CA, P´ erez JA. Reversibility in session-basedconcurrency: A fresh look. Journal of Logic and Algebraic Methods in Programming , 2017. 90:2–30. doi:10.1016/j.jlamp.2017. 03.003

    2017 doi

  67. [76]

    Let it recover: multiparty protoc ol-induced recovery

    Neykova R, Y oshida N. Let it recover: multiparty protoc ol-induced recovery. In: Wu P , Hack S (eds.), CC. ACM Press, 2017 pp. 98–108. doi:10.1145/3 033019

    2017 doi

  68. [77]

    Rever sible sessions with flexible choices

    Castellani I, Dezani-Ciancaglini M, Giannini P . Rever sible sessions with flexible choices. Acta Informatica, 2019. 56(7):553–583. doi:10.1007/s00236-019-00332-y

    2019 doi

  69. [78]

    Reversibility and asymmetri c conflict in event structures

    Phillips IC, Ulidowski I. Reversibility and asymmetri c conflict in event structures. Journal of Logical and Algebraic Methods in Programming , 2015. 84(6):781 – 805. doi:10.1016/j. jlamp.2015.07.004

    2015 doi

  70. [79]

    Towards a categoric al representation of reversible event structures

    Graversen E, Phillips I, Y oshida N. Towards a categoric al representation of reversible event structures. In: V asconcelos VT, Haller P (eds.), PLACES, vo lume 246 of EPTCS. Open Publishing Association, 2017 pp. 49–60. doi:10.4204/EPTC S.246.9

    2017 doi

  71. [80]

    Event structure semantics of (controlled) reversible CCS

    Graversen E, Phillips I, Y oshida N. Event structure semantics of (controlled) reversible CCS. In: Kari J, Ulidowski I (eds.), Reversible Computation, vol ume 11106 of LNCS. Springer, 2018 pp. 122–102. doi:10.1007/978-3-319-99498-7 \ 7

    2018 doi

  72. [81]

    Event structure semantics of reversible p rocess calculi

    Graversen E. Event structure semantics of reversible p rocess calculi. Ph.D. thesis, Imperial College London, 2021

    2021

  73. [82]

    Global types with internal dele- gation

    Castellani I, Dezani-Ciancaglini M, Giannini P , Horne R. Global types with internal dele- gation. Theoretical Computer Science, 2020. 807:128–153. doi:10.1016/j.tcs.2019.09.027. 54 I.Castellani, M.Dezani, P .Giannini/ Types and Semantics for Asynchronous Sessions A. Appendix ...

    2020 doi

  74. [83]

    From (G, Q ) ∈↓ r we get (G′, Q ) ∈↓ r

    Case G = pr!ℓ; G′ and (G′, P ) ∈↓ r. From (G, Q ) ∈↓ r we get (G′, Q ) ∈↓ r. Then (P, Q ) ∈ Rr

  75. [84]

    From (G, Q ) ∈↓ r we get Q = − →π ; Σi∈ I p?ℓi; Qi and (Gi, − →π ; p?ℓi; Qi) ∈↓ r for all i ∈ I

    Case G = ⊞ i∈ I pr!ℓi; Gi and (Gi, p?ℓi; Pi) ∈↓ r for all i ∈ I and |I|> 1. From (G, Q ) ∈↓ r we get Q = − →π ; Σi∈ I p?ℓi; Qi and (Gi, − →π ; p?ℓi; Qi) ∈↓ r for all i ∈ I. Since (p?ℓi; Pi, − →π ; p?ℓi; Qi) ∈ R r for all i ∈ I, by induction Clause (b) is satisfied. Thus− →π = ǫ...

  76. [85]

    From (G, Q ) ∈↓ r we get Q = − →π ′; Σj∈ J q?ℓ′ j; Q′ j and (Gj , − →π ′; q?ℓ′ j; Q′ j) ∈↓ r for all j ∈ J

    Case G = ⊞ j∈ J qr!ℓ′ j; Gj with q ̸= p and P = p?ℓ; − →π ; Σj∈ J q?ℓ′ j; P ′ j and (Gj , p?ℓ; − →π ; q?ℓ′ j; P ′ j) ∈↓ r for all j ∈ J. From (G, Q ) ∈↓ r we get Q = − →π ′; Σj∈ J q?ℓ′ j; Q′ j and (Gj , − →π ′; q?ℓ′ j; Q′ j) ∈↓ r for all j ∈ J. Since (p?ℓ; − →π ; q?ℓ′ j; P ′ j...

  77. [86]

    From (G, Q ) ∈↓ r we get (Gj , Q ) ∈↓ r for all j ∈ J

    Case G = ⊞ j∈ J qs!ℓ′ j; Gj and r ̸= s and r ∈ play(Gj ) and (Gj, P ) ∈↓ r for j ∈ J. From (G, Q ) ∈↓ r we get (Gj , Q ) ∈↓ r for all j ∈ J. Then (P, Q ) ∈ R r

  78. [87]

    Then (G′, P ) ∈↓ r

    Case G = qs?ℓ; G′ and r ∈ play(G′). Then (G′, P ) ∈↓ r. From (G, Q ) ∈↓ r we get (G′, Q ) ∈↓ r. Then (P, Q ) ∈ R r. Lemma 3.10 I f G ∥ M β − → G′ ∥ M ′ is a top transition and G ∥ M is well formed, then G′ ∥ M ′ is well formed too. Proof: If the transition is derived using Rul...

  79. [88]

    If G ↾ p = ⨁ i∈ I q!ℓi; Pi, then G ∥ M pq!ℓi − − − →Gi ∥ M · ⟨p, ℓ i, q⟩ and Gi ↾ p = Pi for all i ∈ I

  80. [89]

    Proof: (1) The proof is by induction on d = depth(G, p)

    If G ↾q = Σi∈ I p?ℓi; Pi and M ≡ ⟨ p, ℓ, q⟩ · M′ for some ℓ, then I = {k} and ℓ = ℓk and G ∥ M pq?ℓk − − − → G′ ∥ M ′ and G′↾q = Pk. Proof: (1) The proof is by induction on d = depth(G, p). Case d = 1 . By definition of projection (see Figure 2), G ↾ p = ⨁ i∈ I q!ℓi; Pi implies...

  81. [90]

    If G ∥ M pq!ℓ − − → G′ ∥ M ′, then M′ ≡ M · ⟨ p, ℓ, q⟩ and G ↾p = ⨁ i∈ I q!ℓi; Pi and ℓ = ℓk and G′↾p = Pk for some k ∈ I and G ↾r ≤ G′↾r for all r ̸= p

  82. [91]

    Proof: (1) By induction on the inference of the transition G ∥ M pq!ℓ − − → G′ ∥ M ′

    If G ∥ M pq?ℓ − − − →G′ ∥ M ′, then M ≡ ⟨ p, ℓ, q⟩ · M′ and G ↾ q = pq?ℓ; G′ ↾ q and G ↾r ≤ G′↾r for all r ̸= q. Proof: (1) By induction on the inference of the transition G ∥ M pq!ℓ − − → G′ ∥ M ′. Base Case. The applied rule must be Rule [EXT-O UT], so G = ⊞ i∈ I pq!ℓi; Gi a...

  83. [92]

    If ρ ≺ ω ρ′ and β ⊲ ω is defined, then β ♦ ρ ≺ β⊲ω β ♦ ρ′

  84. [93]

    If ρ # ρ′ and both β ♦ ρ and β ♦ ρ′ are defined, then β ♦ ρ # β ♦ ρ′

  85. [94]

    If ρ # ρ′, then β ♦ ρ # β ♦ ρ′. Proof: (1) If ρ ≺ ω ρ′, then • either ρ = p :: η and ρ′ = p :: η′ and η < η ′, • or ρ = p :: ζ ·q!ℓ and ρ′ = q :: ζ′ ·p?ℓ and (ω @ p ·ζ) ↱ q ≼ ⋊ ⋉≿ (ω @ q ·ζ′′) ↱ p for some ζ′′and χ such that (ζ′ ·p?ℓ) ↱ p ≼ (ζ′′·p?ℓ·χ ) ↱ p . I.Castellani, M.D...

  86. [95]

    In the second case, let ω ′ = β ◮ ω

    Since η1 < η ′ 1 we conclude β ♦ ρ ≺ β ◮ ω β ♦ ρ′. In the second case, let ω ′ = β ◮ ω . If play(β ) ̸⊂ { p, q}, then β @ p = β @ q = ǫ and β ♦ ρ = ρ and β ♦ ρ′ = ρ′. Moreover, by Definition 8.3(1) (ω ′@ p ) ↱ q = ( ω @ p ) ↱ q and (ω ′@ q ) ↱ p = ( ω @ q ) ↱ p . Therefore (ω @...

  87. [96]

    If both β2 ◮ ω and β2 ◮ (β1 ⊲ ω ) are defined, then β1 ⊲ (β2 ◮ ω ) ∼ = β2 ◮ (β1 ⊲ ω )

  88. [97]

    Proof: (1) Since ω 2 = β2 ◮ ω is defined, by Definition 8.3(1) ω ∼ = β2 ·ω 2 when β2 is an input

    If both β1 ⊲ ω and β2 ⊲ ω are defined, then β1 ⊲ (β2 ⊲ ω ) is defined and β1 ⊲ (β2 ⊲ ω ) ∼ = β2 ⊲ (β1 ⊲ ω ). Proof: (1) Since ω 2 = β2 ◮ ω is defined, by Definition 8.3(1) ω ∼ = β2 ·ω 2 when β2 is an input. Since β2 ◮ (β1 ⊲ ω ) is defined, ω 1 = β1 ⊲ ω is defined and by Definition 8....

  89. [98]

    If β • δ is defined, then β ◦ (β • δ) = δ

    If β ◦ [ω, τ ]∼ is defined, then (β ⊲ ω ) ·β ·τ is well formed and β ◦ [ω, τ ]∼ = [β ⊲ ω, β ⌈(β⊲ω ) τ]∼ Lemma 8.15 1. If β • δ is defined, then β ◦ (β • δ) = δ

  90. [99]

    If β ◦ δ is defined, then β • (β ◦ δ) = δ

  91. [100]

    If both β2 • δ, β2 • (β1 ◦ δ) are defined, and play(β1) ∩ play(β2) = ∅, then β1 ◦ (β2 • δ) = β2 • (β1 ◦ δ)

  92. [101]

    β is required in τ1 ·β ·τ2

    If both β1 ◦ δ, β2 ◦ δ are defined, and play(β1) ∩ play(β2) = ∅, then β1 ◦ (β2 ◦ δ) is defined and β1 ◦ (β2 ◦ δ) = β2 ◦ (β1 ◦ δ). Proof: Statements (1) and (2) immediately follow from Lemma A.1. In the proofs of the remain- ing statements we convene that “ β is required in τ1 ·β...

  93. [102]

    Let τ, τ ′ be such that τ′ is (ω ′·β ·τ)-pointed

    Let β ⊲ ω be defined and ω ′ = β ⊲ ω . Let τ, τ ′ be such that τ′ is (ω ′·β ·τ)-pointed. Then (β ·τ) ⌈ω ′ τ′ = β ⌈ω ′ (τ ⌈ω τ′) Proof: (1) We show (β ·τ) ⌈ω τ′ = β ⌈ω (τ ⌈ω ′ τ′) by induction on τ. Case τ = ǫ. In this case both the LHS and RHS reduce to β ⌈ω τ′, for whatever ω ...

  94. [103]

    If β ⊲ ω is defined, then β ◦ ev(ω, τ ) = ev(β ⊲ ω, β ·τ). Proof: Definition 7.14 and Lemmas A.1 and A.2 with τ′ = ǫ imply (1) and (2) since: (1) β • ev(ω, β ·τ) = β • [ω, (β ·τ) ⌈ω ǫ]∼ by Definition 7.14 = β • [ω, β ⌈ω (τ ⌈ω ′ ǫ)]∼ by Lemma A.2(1) = [ ω ′, τ ⌈ω ′ ǫ]∼ by Lemma A....

  95. [104]

    If δ1 < δ2 and β ◦ δ1 is defined, then β ◦ δ1 < β ◦ δ2

  96. [105]

    Proof: (1) Let δ1 = [ω, τ ]∼ and δ2 = [ω, τ ·τ′]∼

    If δ1 # δ2 and both β ◦ δ1, β ◦ δ2 are defined, then β ◦ δ1 # β ◦ δ2. Proof: (1) Let δ1 = [ω, τ ]∼ and δ2 = [ω, τ ·τ′]∼ . If β • δ1 = [ω ′, τ ]∼ and β • δ2 = [ω ′, τ ·τ′]∼ for some ω ′, then β • δ1 < β • δ2. Let β be an output. If τ ≈ ω β ·τ1 with τ1 ̸= ǫ, then β • δ1 = [ ω ·β,...

  97. [106]

    It follows that τ2 ≈ ω ·β τ ·τ′

  98. [107]

    Let β be an input

    Then we get β • δ1 = [ω ·β, τ ]∼ and β • δ2 = [ω ·β, τ 2]∼ = [ω ·β, τ ·τ′ 2]∼ , which imply β • δ1 < β • δ2. Let β be an input. The proof is similar. (2) Since δ1 < δ 2 and β ◦ δ1 is defined, then also β ◦ δ2 is defined. Let δ1 = [ ω, τ ]∼ and δ2 = [ω, τ ·τ′]∼ . If β ◦ δ1 = [ω ′...

  99. [108]

    If δ ∈ TE (pq?ℓ; G ∥ ⟨p, ℓ, q⟩ · M) and pq?ℓ • δ is defined, then pq?ℓ • δ ∈ TE (G ∥ M)

  100. [109]

    If δ ∈ TE (G ∥ M · ⟨p, ℓ, q⟩), then pq!ℓ ◦ δ ∈ TE (⊞ i∈ I pq!ℓi; Gi ∥ M), where ℓ = ℓk and G = Gk for some k ∈ I

  101. [110]

    If δ ∈ TE (G ∥ M), then pq?ℓ ◦ δ ∈ TE (pq?ℓ; G ∥ ⟨p, ℓ, q⟩ · M). Proof: (1) By Definition 7.17(1), if δ ∈ TE (⊞ i∈ I pq!ℓi; Gi ∥ M ), then δ = ev(ω, τ ), where ω = otr(M) and τ ∈ Tr+(⊞ i∈ I pq!ℓi; Gi), which gives τ ≈ ω pq!ℓh ·τh with τh ∈ Tr+(Gh) for some h ∈ I. By hypothesis ...

  102. [111]

    if δ ∈ TE (G ∥ M) and β • δ is defined, then β • δ ∈ TE (G′ ∥ M ′)

  103. [112]

    Proof: Lemma 8.4 and Session Fidelity (Theorem 3.19) imply otr(M) ∼ = β ⊲ otr(M′)

    if δ ∈ TE (G′ ∥ M ′), then β ◦ δ ∈ TE (G ∥ M). Proof: Lemma 8.4 and Session Fidelity (Theorem 3.19) imply otr(M) ∼ = β ⊲ otr(M′). (1) By induction on the inference of the transition G ∥ M β − → G′ ∥ M ′ , see Figure 5. Base Cases. If the applied rule is [EXT-O UT], then G = ⊞ ...

  104. [113]

    Hence β • δ′ = [ω ′′, τ ′ 1]∼

    Then δ = [ω, pq!ℓk ·τ2]∼ and therefore δ′ = [ω ′, τ 2]∼ = [ω ′, β ·τ′ 1]∼ . Hence β • δ′ = [ω ′′, τ ′ 1]∼ . In Case b we have δ = [ ω, β ·τ1]∼ and p ̸∈ play(β ·τ1). Therefore δ′ = [ ω ′, β ·τ1]∼ . Hence β • δ′ = [ω ′′, τ 1]∼ . In Case c we have δ′ = [ ω ′, τ ′ 0]∼ and β • δ′ =...

  105. [114]

    In Case d we have δ′ = [ω ′, τ 0]∼ and β • δ′ = [ω ′′, τ 0]∼

    = ∅. In Case d we have δ′ = [ω ′, τ 0]∼ and β • δ′ = [ω ′′, τ 0]∼ . So in all cases we conclude that β • δ′ is defined. By induction β •δ′ ∈ TE (G′ k ∥ M ′·⟨p, ℓ k, q⟩). By Lemma 8.17(3) pq!ℓk◦(β •δ′) ∈ TE (G′ ∥ M ′). Since δ′ is defined, Lemma 8.15(1) implies pq!ℓk ◦ δ′ = δ. Si...

  106. [115]

    If 1 ≤ k, l ≤ n, then ¬ (δk # δl)

  107. [116]

    Proof: (1) Let δi = [ω, τ i]∼ for all i, 1 ≤ i ≤ n

    τ[i] = i/ o(δi) for all i, 1 ≤ i ≤ n. Proof: (1) Let δi = [ω, τ i]∼ for all i, 1 ≤ i ≤ n. By Definitions 8.19 and 7.14 τi = τ[1 ... i] ⌈ω ǫ. By Definition 7.13 if τi @ p ̸= ǫ, then there are ki ≤ i and τ′ i such that play(τ[ki]) = {p}, p ̸∈ play(τ′ i ) and τi = τ[1 ... ki − 1] ⌈...

  108. [117]

    If tec(ω, τ ) = δ1; · · ·; δn and tec(ω ′, τ ′) = δ′ 2; · · ·; δ′ n, then β ◦ δ′ i = δi for all i, 2 ≤ i ≤ n

    Let τ = β ·τ′ and ω = β ⊲ ω ′. If tec(ω, τ ) = δ1; · · ·; δn and tec(ω ′, τ ′) = δ′ 2; · · ·; δ′ n, then β ◦ δ′ i = δi for all i, 2 ≤ i ≤ n. Proof: The proof is by induction on τ. (1) By Definition 8.19 δi = ev(ω, β ·τ′[1 ... i]) and δ′ i = ev(ω ′, τ ′[1 ... i]) for all i, 2 ≤ ...

Pith tools

Reviewed May 24, 2026 · model on record in the stance chip above.