Message-Observing Sessions
Fuente:
arXiv
Enregistré dans:
| Auteurs principaux: | , |
|---|---|
| Format: | Preprint |
| Publié: |
2024
|
| Sujets: | |
| Accès en ligne: | |
| Tags: |
Ajouter un tag
Pas de tags, Soyez le premier à ajouter un tag!
|
| _version_ | 1866911790969913344 |
|---|---|
| author | Kavanagh, Ryan Pientka, Brigitte |
| author_facet | Kavanagh, Ryan Pientka, Brigitte |
| contents | We present Most, a process language with message-observing session types. Message-observing session types extend binary session types with type-level computation to specify communication protocols that vary based on messages observed on other channels. Hence, Most allows us to express global invariants about processes, rather than just local invariants, in a bottom-up, compositional way. We give Most a semantic foundation using traces with binding, a semantic approach for compositionally reasoning about traces in the presence of name generation. We use this semantics to prove type soundness and compositionality for Most processes. We see this as a significant step towards capturing message-dependencies and providing more precise guarantees about processes. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2403_04633 |
| institution | arXiv |
| publishDate | 2024 |
| record_format | arxiv |
| spellingShingle | Message-Observing Sessions Kavanagh, Ryan Pientka, Brigitte Programming Languages D.3.3; F.3.2 We present Most, a process language with message-observing session types. Message-observing session types extend binary session types with type-level computation to specify communication protocols that vary based on messages observed on other channels. Hence, Most allows us to express global invariants about processes, rather than just local invariants, in a bottom-up, compositional way. We give Most a semantic foundation using traces with binding, a semantic approach for compositionally reasoning about traces in the presence of name generation. We use this semantics to prove type soundness and compositionality for Most processes. We see this as a significant step towards capturing message-dependencies and providing more precise guarantees about processes. |
| title | Message-Observing Sessions |
| topic | Programming Languages D.3.3; F.3.2 |
| url | https://arxiv.org/abs/2403.04633 |