一句话：提出 TOAST，用时间约束安全支持异步混合选择，从而在会话类型中建模超时并保证进展。
异步通信模型中，混合选择会破坏通信有限状态机关键性质的可判定性，因此长期被会话类型所禁止，也阻碍了对 Web 与云服务中常见超时行为的建模。本文提出二元超时异步会话类型 TOAST，作为二元异步定时会话类型的扩展，通过时间约束来规范混合选择的使用，以保持通信安全。作者为 TOAST 给出新的行为语义，证明在存在混合选择时系统仍可保证进展；并在此基础上设计带进程定时器的演算，以类似 Erlang 的 receive-after 模式表达超时，建立与 TOAST 规约对应的类型系统，并证明主体归约。评估主要基于形式化定义与元理论证明。
Mixed-choice has long been barred from models of asynchronous communication since it compromises the decidability of key properties of communicating finite-state machines. Session types inherit this restriction, which precludes them from fully modelling timeouts -- a core property of web and cloud services. To address this deficiency, we present (binary) Timeout Asynchronous Session Types (TOAST) as an extension to (binary) asynchronous timed session types, that permits mixed-choice. TOAST deploys timing constraints to regulate the use of mixed-choice so as to preserve communication safety. We provide a new behavioural semantics for TOAST which guarantees progress in the presence of mixed-choice. Building upon TOAST, we provide a calculus featuring process timers which is capable of modelling timeouts using a receive-after pattern, much like Erlang, and capture the correspondence with TOAST specifications via a type system for which we prove subject reduction.
DOI 原文 · arXiv · PDF（开放获取） · DBLP
@article{PearsBMK25,
title = {Timeout Asynchronous Session Types: Safe Asynchronous Mixed-Choice For Timed Interactions},
author = {Jonah Pears and Laura Bocchi and Maurizio Murgia and Andy King},
journal = {Logical Methods in Computer Science},
volume = {Volume 21, Issue 3},
year = {2025},
doi = {10.46298/lmcs-21(3:6)2025}
}