20.500.12556/RUL-167167 Higher-order asynchronous effects We explore asynchronous programming with algebraic effects. We complement their conventional synchronous treatment by showing how to naturally also accommodate asynchrony within them, namely, by decoupling the execution of operation calls into signalling that an operation's implementation needs to be executed, and interrupting a running computation with the operation's result, to which the computation can react by installing interrupt handlers. We formalise these ideas in a small core calculus and demonstrate its flexibility using 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. In addition, the paper is accompanied by a formalisation of the calculus's type safety proofs in Agda, and a prototype implementation in OCaml. algebraic effects asynchrony concurrency interrupt handling signals promises true false true Angleški jezik Angleški jezik Članek v reviji 2025-02-11 12:31:31 2025-02-11 12:31:36 2025-02-12 04:22:51 0000-00-00 00:00:00 2024 0 0 Str. 26:1-26:50 iss. 3, [article no.] 26 Vol. 20 2024 0000-00-00 Zaloznikova Objavljeno NiDoloceno 0000-00-00 0000-00-00 2024-01-01 004.42:510.6 1860-5974 10.46298/lmcs-20(3:26)2024 225766915 2307.13795.pdf 2307.13795.pdf 1 FD595435D8676869A87AAD5AAAE5F5C0 c197b383eb27766f5c5de4ef7221e2a0fc67f63c76161be321667c3bc2ee5f35 13d30b10-e86c-11ef-b232-0050569b8976 https://repozitorij.uni-lj.si/Dokument.php?lang=slv&id=199391 https://lmcs.episciences.org/14321 1 dfeb9204-e86a-11ef-b232-0050569b8976 https://repozitorij.uni-lj.si/Dokument.php?lang=slv&id=199390 Fakulteta za matematiko in fiziko 0 0 0