MAGπ!：复制在易错通信类型化中的作用
编程语言
2024-04-26 v1
摘要
MAGπ是一种多参与方、异步且泛化的π演算，它将超时引入会话类型，以推理易错通信。其类型系统保证所有可能的消息丢失都由超时分支处理。在这项工作中，我们认为之前的做法过于严格。我们提出了MAGπ!，这是一个扩展，首次将复制引入多方会话类型（MPST）。复制是π演算中用于建模无限可用服务器的标准构造。我们将此构造提升到类型层面，并表明它简化了分布式客户端-服务器交互的规范。我们证明了与泛化MPST相关的性质：主题归约、会话保真度和进程性质验证。
引用
@article{arxiv.2404.16213,
title = {MAG$\pi$!: The Role of Replication in Typing Failure-Prone Communication},
author = {Matthew Alan Le Brun and Ornela Dardha},
journal= {arXiv preprint arXiv:2404.16213},
year = {2024}
}