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 $\mathtt{receive\text{-}after}$ pattern, much like Erlang, and capture the correspondence with TOAST specifications via a type system for which we prove subject reduction.

翻译：长期以来，混合选择一直被排除在异步通信模型之外，因为它会损害通信有限状态机关键属性的可判定性。会话类型继承了这一限制，使其无法完全建模超时（网络和云服务的核心属性）。为解决这一缺陷，我们提出（二元）超时异步会话类型（TOAST），作为（二元）异步定时会话类型的扩展，允许混合选择。TOAST部署定时约束来规范混合选择的使用，从而保障通信安全性。我们为TOAST提供了一种新的行为语义，确保在存在混合选择的情况下仍能保证进展性。基于TOAST，我们提出一种包含进程定时器的演算，能够通过类似Erlang的$\mathtt{receive\text{-}after}$模式建模超时，并通过类型系统捕获与TOAST规范之间的对应关系，我们证明了该类型系统的主体归约性质。