Digital repository of Slovenian research organisations

Show document
A+ | A- | Help | SLO | ENG

Title:Higher-order asynchronous effects
Authors:ID Ahman, Danel (Author)
ID Pretnar, Matija (Author)
Files:.pdf PDF - Presentation file, download (991,10 KB)
MD5: B9DFC810E703FE82389CCBB2AFB8E70E
 
URL URL - Source URL, visit https://lmcs.episciences.org/14321
 
Language:English
Typology:1.01 - Original Scientific Article
Organization:Logo IMFM - Institute of Mathematics, Physics, and Mechanics
Abstract: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.
Keywords:algebraic effects, asynchrony, concurrency, interrupt handling, signals, promises
Publication status:Published
Publication version:Version of Record
Publication date:01.01.2024
Year of publishing:2024
Number of pages:str. 26:1-26:50
Numbering:Vol. 20, iss. 3, [article no.] 26
PID:20.500.12556/DiRROS-21473 New window
UDC:004.42:510.6
ISSN on article:1860-5974
DOI:10.46298/lmcs-20(3:26)2024 New window
COBISS.SI-ID:225766915 New window
Note:
Publication date in DiRROS:11.02.2025
Views:379
Downloads:282
Metadata:XML DC-XML DC-RDF
:
Copy citation
  
Share:Bookmark and Share


Hover the mouse pointer over a document title to show the abstract or click on the title to get all document metadata.

Record is a part of a journal

Title:Logical methods in computer science
Shortened title:Log. methods comput. sci.
Publisher:Institut für Theoretische Informatik, Technische Universität Braunschweig.
ISSN:1860-5974
COBISS.SI-ID:16816473 New window

Document is financed by a project

Funder:Other - Other funder or multiple funders
Funding programme:European Union’s Horizon 2020 research and innovation programme under the Marie Skłodowska-Curie grant
Project number:No 834146

Funder:Other - Other funder or multiple funders
Funding programme:Air Force Office of Scientific Research
Project number:FA9550-17-1-0326

Funder:Other - Other funder or multiple funders
Funding programme:Air Force Office of Scientific Research
Project number:FA9550-21-1-0024

Licences

License:CC BY 4.0, Creative Commons Attribution 4.0 International
Link:http://creativecommons.org/licenses/by/4.0/
Description:This is the standard Creative Commons license that gives others maximum freedom to do what they want with the work as long as they credit the author.

Back