Danel Ahman: Strong normalisation for a language with asynchronous algebraic effects

Abstract: A few of years ago, I and Matija Pretnar proposed an effectful lambda calculus for asynchronous programming with algebraic effects, based on programs sending out signals, receiving interrupts, and reacting to the latter by installing interrupt handlers. This lambda calculus was flexible enough to account for examples ranging from a multi-party web application, to pre-emptive multi-threading, to (cancellable) remote function calls, to a parallel variant of runners of algebraic effects.

Since early on, we conjectured that certain fragments of this lambda calculus ought to be strongly normalising, i.e., all reduction sequences starting from well-typed programs written in those fragments ought to have finite length. In this talk, I will report on some recent progress in proving one important fragment of this lambda calculus strongly normalising, demonstrate that another fragment we conjectured to be strongly normalising isn't so, and discuss how one might overcome that problem and extend the strong normalisation proof further. The normalisation proof is based Tait's notion of reducibility and its extension to computational effects by Lindley and Stark, both of which I will explain for background in the talk.

This is joint work with Ilja Sobolev.