Любопытный пейпер: «Asynchronous effects»
https://arxiv.org/pdf/2003.02110.pdf
TL;DR: авторы представляют небольшое лямбда-исчисление λæ для описания асинхронных алгебраических эффектов, язык на его основе AEff, и его формализацию на Агде. Выдержка из аннотации:
«At the heart of our approach is the decoupling of the execution of operation calls into signalling that the operation’s implementation needs to be executed and interrupting the computation with the operation’s result, to which the computation can react through a previously installed interrupt handler.»