Back to Search
Start Over
Deconfined Global Types for Asynchronous Sessions
- Source :
- Logical Methods in Computer Science, Volume 19, Issue 1 (January 13, 2023) lmcs:8752
- Publication Year :
- 2021
-
Abstract
- Multiparty sessions with asynchronous communications and global types play an important role for the modelling of interaction protocols in distributed systems. In designing such calculi the aim is to enforce, by typing, good properties for all participants, maximising, at the same time, the accepted behaviours. Our type system improves the state-of-the-art by typing all asynchronous sessions and preserving the key properties of Subject Reduction, Session Fidelity and Progress when some well-formedness conditions are satisfied. The type system comes together with a sound and complete type inference algorithm. The well-formedness conditions are undecidable, but an algorithm checking an expressive restriction of them recovers the effectiveness of typing.
Details
- Database :
- arXiv
- Journal :
- Logical Methods in Computer Science, Volume 19, Issue 1 (January 13, 2023) lmcs:8752
- Publication Type :
- Report
- Accession number :
- edsarx.2111.11984
- Document Type :
- Working Paper
- Full Text :
- https://doi.org/10.46298/lmcs-19(1:3)2023