Asynchronous effects of Ahman and Pretnar complement the conventional synchronous treatment of algebraic effects with asynchrony based on decoupling the execution of algebraic operation calls into signalling that an operation's implementation needs to be executed, and into interrupting a running computation with the operation's result, to which the computation can react by installing matching interrupt handlers. Beyond providing asynchrony for algebraic effects, the resulting core calculus also naturally models examples such as pre-emptive multi-threading, (cancellable) remote function calls, and multi-party applications. In this paper, we study the normalisation properties of this calculus. We prove that if one removes general recursion from it, then the remaining calculus is strongly normalising, including both its sequential and parallel parts. To cover more interesting programs, we also prove that the sequential part of the calculus remains strongly normalising when a controlled amount of interrupt-driven recursive behaviour is reintroduced. Our normalisation proofs are structured compositionally as an extension of Lindley and Stark's $\top\top$-lifting-based approach for proving strong normalisation of effectful languages. All our results are also formalised in Agda.

翻译：Ahman和Pretnar提出的异步效应用异步性补充了代数效应的传统同步处理方式，其核心思想是将代数操作调用的执行解耦为：发出需要执行操作实现的信号，以及用操作结果中断运行中的计算，计算可通过安装匹配的中断处理程序来响应这些结果。该核心演算不仅为代数效应提供了异步支持，还自然建模了抢占式多线程、（可取消的）远程函数调用及多方应用等实例。本文研究该演算的规范化性质，证明若移除其中的一般递归，则剩余演算（包括其顺序部分和并行部分）具有强规范化。为覆盖更有趣的程序，我们还证明当引入受控量的中断驱动递归行为时，演算的顺序部分仍保持强规范化。我们的规范化证明采用组合式结构，扩展了Lindley和Stark基于$\top\top$提升的含效应语言强规范化证明方法。所有结果均在Agda中形式化。