pith. sign in

arxiv: 2102.00865 · v8 · submitted 2021-02-01 · 💻 cs.LO

Global types and event structure semantics for asynchronous multiparty sessions

Ilaria Castellani (INDES , Inria , UCA) , Mariangiola Dezani-Ciancaglini (UNITO) , Paola Giannini (UPO) This is my paper

Pith reviewed 2026-05-24 13:30 UTC · model grok-4.3

classification 💻 cs.LO
keywords global typesevent structuresasynchronous communicationmultiparty sessionssession typessemanticsprogress
0
0 comments X

The pith

The event structure of a typable asynchronous multiparty session equals the event structure of its global type.

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

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.

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.

What carries the argument

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

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.

Where Pith is reading between the lines

These are 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.

Load-bearing premise

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

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.

Figures

Figures reproduced from arXiv: 2102.00865 by Ilaria Castellani (INDES, Inria, Mariangiola Dezani-Ciancaglini (UNITO), Paola Giannini (UPO), UCA).

Figure 1
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. Figure 2: Projection of global types onto participants. [PITH_FULL_IMAGE:figures/full_fig_p008_2.png] view at source ↗
Figure 3
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 ↗
Figure 4
Figure 4. Figure 4: Preorder on processes and network typing rule. [PITH_FULL_IMAGE:figures/full_fig_p012_4.png] view at source ↗
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 asynchronous type pq?ℓ1; pr!ℓ; pr?ℓ k hp, ℓ1, qi [PITH_FULL_IMAGE:figures/full_fig_p013_5.png] view at source ↗
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] view at source ↗
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] view at source ↗
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] view at source ↗
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.

Editorial analysis

A structured set of objections, weighed in public.

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

Referee Report

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

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.

Axiom & Free-Parameter Ledger

0 free parameters · 1 axioms · 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.

axioms (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.

pith-pipeline@v0.9.0 · 5627 in / 1189 out tokens · 24860 ms · 2026-05-24T13:30:27.991563+00:00 · methodology

discussion (0)

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

Reference graph

Works this paper leans on

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]

    Language primitives and type discipline for structured communication-based programming

    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]

    doi:10.1145/2827695

    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]

    From communicating machine s to graphical choreographies

    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

  9. [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

    work page doi:10.1016/j.jlamp.2017.11.002 2018

  10. [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

    work page doi:10.1007/978-3-642-15375-4 2010

  11. [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

    work page doi:10.1145/2003476.2003499 2011

  12. [12]

    Propositions as sessions

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

    work page doi:10.1017/s095679681400001x 2014

  13. [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

    work page doi:10.1016/j.ic.2014.08.001 2014

  14. [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

    work page doi:10.1017/s0960129514000218 2016

  15. [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

    work page arXiv 2022

  16. [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 .Giannini/ Types and Semantics for Asynchronous Sessions

    work page 1988

  17. [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

    work page 2015

  18. [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, 1988 pp. 411–427. doi:10.1007/BFb0013028

    work page doi:10.1007/bfb0013028 1988

  19. [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

    work page doi:10.1006/inco.1994 1994

  20. [20]

    Events in computation

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

    work page 1980

  21. [21]

    Nielsen, G

    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

    work page doi:10.1016/0304-3975(81)90112-2 1981

  22. [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

    work page doi:10.1007/978-3-642-00590-9 2009

  23. [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

    work page doi:10.1016/j.ic.2017.07.010 2017

  24. [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

    work page 2017

  25. [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

    work page doi:10.1016/0304-3975(83)90059-2 1983

  26. [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

    work page doi:10.1145/3290343 2019

  27. [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

    work page arXiv 2021

  28. [28]

    Types and Programming Languages

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

    work page 2002

  29. [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

    work page doi:10.1145/1926385.19 2011

  30. [30]

    MSCS760(2015)

    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

    work page doi:10.1017/s0960129514000188 2016

  31. [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

    work page doi:10.1007/s00236-005-0177-z 2005

  32. [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

    work page doi:10.1007/978-3-642-23217-6 2011

  33. [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–108. doi:10.1007/978-3-319-30936-1 \ 5. I.Castellani, M.Dezani, P .Giannini/ Typ...

    work page doi:10.1007/978-3-319-30936-1 2016

  34. [34]

    Composition and decomposition of multiparty sessions , journal =

    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

    work page doi:10.1016/j.jlamp.2020.100620 2021

  35. [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

    work page 2016

  36. [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

    work page 1991

  37. [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 Occasion of His 65th Birthday, volume 11665 of LNCS. Springer, 2019 pp. 340–363. ...

    work page doi:10.1007/978-3-030-21485-2 2019

  38. [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

    work page doi:10.1007/bfb0084778 1992

  39. [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

    work page doi:10.1017/s096012950007002x 1996

  40. [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,

    work page

  41. [41]

    doi:10.1007/s00236-005-0179-x

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

    work page doi:10.1007/s00236-005-0179-x

  42. [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

    work page doi:10.1016/s0890-5401(02)93171-8 2002

  43. [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

    work page 2006

  44. [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

    work page doi:10.1145/237 2012

  45. [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

    work page doi:10.2168/lmcs-11(4:13)2015 2015

  46. [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

    work page doi:10.3233/fi-2019-1863 2019

  47. [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

    work page doi:10.1016/j.tcs.2018.02.010 2018

  48. [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 ,

    work page

  49. [49]

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

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

    work page doi:10.23638/lmcs-17(1:20)2021 2021

  50. [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

    work page doi:10.1145/3434297 2021

  51. [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

    work page 1982

  52. [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

    work page doi:10.1007/3-540-17660-8 1987

  53. [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

    work page doi:10.1109/lics.1988.5112 1988

  54. [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

    work page doi:10.1016/0304-3975(90)90095-y 1990

  55. [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

    work page doi:10.1145/828.833 1984

  56. [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

    work page doi:10.1007/3-540-17906-2 1986

  57. [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

    work page doi:10.3233/fi-1991-14103 1991

  58. [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

    work page 1994

  59. [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

    work page 1993

  60. [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

    work page 1996

  61. [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

    work page doi:10.1007/978-3-540-74407-8 2007

  62. [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

    work page doi:10.1016/j.tcs.2010.01.024 2010

  63. [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–

    work page 2012

  64. [65]

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

    work page doi:10.1007/978-3-642-28729-9

  65. [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

    work page 2015

  66. [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

    work page doi:10.1007/978-3-319-25150-9 2015

  67. [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

    work page doi:10.1007/978-3-319-40578-0 2016

  68. [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 for Asynchronous Sessions 53

    work page doi:10.4204/eptcs.324.6 2020

  69. [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

    work page doi:10.1109/lics.2011.13 2011

  70. [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

    work page doi:10.1007/978-3-662-54458-7 2017

  71. [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

    work page doi:10.4204/eptcs.155.3 2014

  72. [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

    work page doi:10.1007/978-3-319-40578- 2016

  73. [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

    work page doi:10.1145/3131851.3131864 2017

  74. [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

    work page doi:10.1016/j.jlamp.2017 2017

  75. [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

    work page doi:10.1145/3 2017

  76. [77]

    Acta Informatica , author =

    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

    work page doi:10.1007/s00236-019-00332-y 2019

  77. [78]

    Masset, R

    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

    work page doi:10.1016/j 2015

  78. [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

    work page doi:10.4204/eptc 2017

  79. [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

    work page doi:10.1007/978-3-319-99498-7 2018

  80. [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

    work page 2021

Showing first 80 references.