A Formal Model for Direct-style Asynchronous Observables

TL;DR

This paper introduces a formal model combining Async programming with reactive observable streams, ensuring protocol adherence and type safety in asynchronous reactive programming.

Contribution

It formalizes the unified Reactive Async model within an object-based calculus, capturing asynchronous observable protocols and proving their preservation.

Findings

Formalization of Reactive Async model in core calculus

Proof of subject reduction theorem ensuring protocol preservation

Guarantee of protocol adherence for well-typed programs

Abstract

Languages like F#, C#, and recently also Scala, provide "Async" programming models which aim to make asynchronous programming easier by avoiding an inversion of control that is inherent in callback-based programming models. This paper presents a novel approach to integrate the Async model with observable streams of the Reactive Extensions model. Reactive Extensions are best-known from the .NET platform, and widely-used implementations of its programming model exist also for Java, Ruby, and other languages. This paper contributes a formalization of the unified "Reactive Async" model in the context of an object-based core calculus. Our formal model captures the essence of the protocol of asynchronous observables using a heap evolution property. We prove a subject reduction theorem; the theorem implies that reduction preserves the heap evolution property. Thus, for well-typed programs our calculus ensures the protocol of asynchronous observables.