Conference item
Denotational reasoning for asynchronous multiparty session types
- 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.
- Publication status:
- Published
- Peer review status:
- Peer reviewed
Actions
Access Document
- Files:
-
-
(Preview, Accepted manuscript, pdf, 794.0KB, Terms of use)
-
- Publisher copy:
- 10.1007/978-3-032-22723-2_3
Authors
+ UK Research and Innovation
More from this funder
- Funder identifier:
- https://ror.org/001aqnf71
- Grant:
- 10066667
+ Engineering and Physical Sciences Research Council
More from this funder
- Funder identifier:
- https://ror.org/0439y7842
- Grant:
- EP/T006544/2
- EP/T014709/2
- Publisher:
- Springer
- Host title:
- Programming Languages and Systems 35th European Symposium on Programming, ESOP 2026, Held as Part of the International Joint Conferences on Theory and Practice of Software, ETAPS 2026, Turin, Italy, April 11–16, 2026, Proceedings, Part II
- Pages:
- 64–93
- Series:
- Lecture Notes in Computer Science
- Series number:
- 16502
- Publication date:
- 2026-04-10
- Acceptance date:
- 2025-12-22
- Event title:
- 35th European Symposium on Programming (ESOP 2026)
- Event location:
- Turin, Italy
- Event website:
- https://etaps.org/2026/conferences/esop/
- Event start date:
- 2026-04-11
- Event end date:
- 2026-04-16
- DOI:
- EISSN:
-
1611-3349
- ISSN:
-
0302-9743
- EISBN:
- 9783032227232
- ISBN:
- 9783032227225
- Language:
-
English
- Keywords:
- Pubs id:
-
2359899
- Local pid:
-
pubs:2359899
- Deposit date:
-
2026-01-15
- ARK identifier:
Terms of use
- Copyright holder:
- McDermott and Yoshida
- Copyright date:
- 2026
- Rights statement:
- © 2026 The Editor(s) (if applicable) and The Author(s), under exclusive license to Springer Nature Switzerland AG
- Notes:
- This paper will be presented at the 35th European Symposium on Programming (ESOP 2026), 11th-16th April 2026, Turin, Italy. The author accepted manuscript (AAM) of this paper has been made available under the University of Oxford's Open Access Publications Policy, and a CC BY public copyright licence has been applied.
- Licence:
- CC Attribution (CC BY)
If you are the owner of this record, you can report an update to it here: Report update to this record