Strong Normalisation for Asynchronous Effects
Danel Ahman, Ilja Sobolev
TL;DR
The paper investigates termination guarantees for the core calculus $\lambda_{\ae}$ of asynchronous algebraic effects, which models asynchronous operation calls via signals, interrupts, and interrupt handlers alongside blocking awaits. It develops a type-directed reducibility framework based on $\top\top$-lifting (an extension of Girard–Tait techniques) and Kripke-style indexing to handle the interplay of sequential and parallel computations and their effects, proving strong normalisation for the recursion-free sequential fragment, and for a restricted reinstallable-interrupt-handlers variant. It further shows that reinstantiating interrupt handlers breaks SN in parallel settings unless carefully constrained, and provides a strongly normalising variant that encodes reinstallability with sum types in handler return values. The results are formalised in Agda, providing rigorous termination guarantees for expressive asynchronous computations and guiding the design of safe higher-order effectful languages with dynamic concurrency features.
Abstract
Asynchronous effects of Ahman and Pretnar complement the conventional synchronous treatment of algebraic computational 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, multi-party applications, and even a parallel variant of runners of algebraic effects. In this paper, we study the normalisation properties of this calculus. We prove that if one removes general recursion from the original calculus, then the remaining calculus is strongly normalising, including both its sequential and parallel parts. However, this only guarantees termination for very simple asynchronous examples. To improve on this result, we also prove that the sequential fragment of the calculus remains strongly normalising when a controlled amount of interrupt-driven recursive behaviour is reintroduced. Our strong normalisation proofs are structured compositionally as a natural 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.