Strong Normalisation for Asynchronous Effects
Fuente:
arXiv
Guardado en:
| Autores principales: | , |
|---|---|
| Formato: | Preprint |
| Publicado: |
2026
|
| Materias: | |
| Acceso en línea: | |
| Etiquetas: |
Agregar Etiqueta
Sin Etiquetas, Sea el primero en etiquetar este registro!
|
| _version_ | 1866911634433245184 |
|---|---|
| author | Ahman, Danel Sobolev, Ilja |
| author_facet | Ahman, Danel Sobolev, Ilja |
| contents | 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. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2602_05528 |
| institution | arXiv |
| publishDate | 2026 |
| record_format | arxiv |
| spellingShingle | Strong Normalisation for Asynchronous Effects Ahman, Danel Sobolev, Ilja Programming Languages Logic in Computer Science 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. |
| title | Strong Normalisation for Asynchronous Effects |
| topic | Programming Languages Logic in Computer Science |
| url | https://arxiv.org/abs/2602.05528 |