Strong Normalisation for Asynchronous Effects

TL;DR

This paper proves strong normalization for a calculus modeling asynchronous algebraic effects, including extensions with limited recursion, using a structured proof approach formalized in Agda.

Contribution

It establishes strong normalization results for an asynchronous effects calculus with recursion restrictions, extending prior methods with a formal Agda proof.

Findings

The calculus is strongly normalising without recursion.

Sequential parts remain strongly normalising with limited recursion.

Proofs are formalized in Agda.

Abstract

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.