Change search
CiteExportLink to record
Permanent link

Direct link
Cite
Citation style
  • apa
  • harvard1
  • ieee
  • modern-language-association-8th-edition
  • vancouver
  • Other style
More styles
Language
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Other locale
More languages
Output format
  • html
  • text
  • asciidoc
  • rtf
A reduction semantics for direct-style asynchronous observables
KTH, School of Electrical Engineering and Computer Science (EECS).ORCID iD: 0000-0002-2659-5271
Carnegie Mellon Univ, Pittsburgh, PA 15213 USA..
2019 (English)In: The Journal of logical and algebraic methods in programming, ISSN 2352-2208, E-ISSN 2352-2216, Vol. 105, p. 75-111Article in journal (Refereed) Published
Abstract [en]

Asynchronous programming has gained in importance, not only due to hardware developments like multi-core processors, but also due to pervasive asynchronicity in client-side Web programming and large-scale Web applications. However, asynchronous programming is challenging. For example, control-flow management and error handling are much more complex in an asynchronous than a synchronous context. Programming with asynchronous event streams is especially difficult: expressing asynchronous stream producers and consumers requires explicit state machines in continuation-passing style when using widely-used languages like Java. In order to address this challenge, recent language designs like Google's Dart introduce asynchronous generators which allow expressing complex asynchronous programs in a familiar blocking style while using efficient non-blocking concurrency control under the hood. However, several issues remain unresolved, including the integration of analogous constructs into statically-typed languages, and the formalization and proof of important correctness properties. This paper presents a design for asynchronous stream generators for Scala, thereby extending previous facilities for asynchronous programming in Scala from tasks/futures to asynchronous streams. We present a complete formalization of the programming model based on a reduction semantics and a static type system. Building on the formal model, we contribute a complete type soundness proof, as well as the proof of a subject reduction theorem which establishes that the programming model enforces an important state transition protocol for asynchronous streams. (C) 2019 Elsevier Inc. All rights reserved.

Place, publisher, year, edition, pages
ELSEVIER SCIENCE INC , 2019. Vol. 105, p. 75-111
National Category
Computer and Information Sciences
Identifiers
URN: urn:nbn:se:kth:diva-252590DOI: 10.1016/j.jlamp.2019.03.002ISI: 000467670900004OAI: oai:DiVA.org:kth-252590DiVA, id: diva2:1322807
Note

QC 20190611

Available from: 2019-06-11 Created: 2019-06-11 Last updated: 2019-06-11Bibliographically approved

Open Access in DiVA

No full text in DiVA

Other links

Publisher's full text

Authority records BETA

Haller, Philipp

Search in DiVA

By author/editor
Haller, Philipp
By organisation
School of Electrical Engineering and Computer Science (EECS)
In the same journal
The Journal of logical and algebraic methods in programming
Computer and Information Sciences

Search outside of DiVA

GoogleGoogle Scholar

doi
urn-nbn

Altmetric score

doi
urn-nbn
Total: 63 hits
CiteExportLink to record
Permanent link

Direct link
Cite
Citation style
  • apa
  • harvard1
  • ieee
  • modern-language-association-8th-edition
  • vancouver
  • Other style
More styles
Language
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Other locale
More languages
Output format
  • html
  • text
  • asciidoc
  • rtf