Збережено в:
| Автори: | , |
|---|---|
| Формат: | Preprint |
| Опубліковано: |
2024
|
| Предмети: | |
| Онлайн доступ: | https://arxiv.org/abs/2404.16213 |
| Теги: |
Додати тег
Немає тегів, Будьте першим, хто поставить тег для цього запису!
|
Зміст:
- MAG$π$ is a Multiparty, Asynchronous and Generalised $π$-calculus that introduces timeouts into session types as a means of reasoning about failure-prone communication. Its type system guarantees that all possible message-loss is handled by timeout branches. In this work, we argue that the previous is unnecessarily strict. We present MAG$π$!, an extension serving as the first introduction of replication into Multiparty Session Types (MPST). Replication is a standard $π$-calculus construct used to model infinitely available servers. We lift this construct to type-level, and show that it simplifies specification of distributed client-server interactions. We prove properties relevant to generalised MPST: subject reduction, session fidelity and process property verification.