Mixed-choice has long been barred from models of asynchronous communication since it compromises key properties of communicating finite-state machines. Session types inherit this restriction, which precludes them from fully modelling timeouts -- a key programming feature to handle failures. To address this deficiency, we present (binary) TimeOut Asynchronous Session Types ({TOAST}) as an extension to (binary) asynchronous timed session types to permit mixed-choice. {TOAST} deploy 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 informally illustrate the correspondence with TOAST specifications.

翻译：混合选择长期以来一直被排除在异步通信模型之外，因为它破坏了通信有限状态机的关键属性。会话类型继承了这一限制，使其无法完全建模超时——这是处理故障的关键编程特性。为解决这一缺陷，我们提出了（二元）超时异步会话类型（TOAST），作为（二元）异步定时会话类型的扩展，以允许混合选择。TOAST利用定时约束来规范混合选择的使用，从而保障通信安全性。我们为TOAST提供了一种新的行为语义，确保在存在混合选择的情况下仍能保持进展。基于TOAST，我们提供了一个包含进程定时器的演算，该演算能够使用类似Erlang的$\mathtt{receive\text{-}after}$模式来建模超时，并非正式地说明了与TOAST规范的对应关系。