Fair Termination of Asynchronous Binary Sessions
Fuente:
arXiv
Saved in:
| Main Authors: | , |
|---|---|
| Format: | Preprint |
| Published: |
2025
|
| Subjects: | |
| Online Access: | |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| _version_ | 1866929759170068480 |
|---|---|
| author | Padovani, Luca Zavattaro, Gianluigi |
| author_facet | Padovani, Luca Zavattaro, Gianluigi |
| contents | We study a theory of asynchronous session types ensuring that well-typed processes terminate under a suitable fairness assumption. Fair termination entails starvation freedom and orphan message freedom namely that all messages, including those that are produced early taking advantage of asynchrony, are eventually consumed. The theory is based on a novel fair asynchronous subtyping relation for session types that is coarser than the existing ones. The type system is also the first of its kind that is firmly rooted in linear logic: fair asynchronous subtyping is incorporated as a natural generalization of the cut and axiom rules of linear logic and asynchronous communication is modeled through a suitable set of commuting conversions and of deep cut reductions in linear logic proofs. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2503_07273 |
| institution | arXiv |
| publishDate | 2025 |
| record_format | arxiv |
| spellingShingle | Fair Termination of Asynchronous Binary Sessions Padovani, Luca Zavattaro, Gianluigi Programming Languages Distributed, Parallel, and Cluster Computing Logic in Computer Science F.3.1; F.3.2; F.3.3 We study a theory of asynchronous session types ensuring that well-typed processes terminate under a suitable fairness assumption. Fair termination entails starvation freedom and orphan message freedom namely that all messages, including those that are produced early taking advantage of asynchrony, are eventually consumed. The theory is based on a novel fair asynchronous subtyping relation for session types that is coarser than the existing ones. The type system is also the first of its kind that is firmly rooted in linear logic: fair asynchronous subtyping is incorporated as a natural generalization of the cut and axiom rules of linear logic and asynchronous communication is modeled through a suitable set of commuting conversions and of deep cut reductions in linear logic proofs. |
| title | Fair Termination of Asynchronous Binary Sessions |
| topic | Programming Languages Distributed, Parallel, and Cluster Computing Logic in Computer Science F.3.1; F.3.2; F.3.3 |
| url | https://arxiv.org/abs/2503.07273 |