A Graph-Based Formal Semantics of Reactive Programming

In recent years, stream processing has become the de facto paradigm to process any kind of real-time data in many kinds of applications. Different libraries, frameworks and techniques exists which aim to make it easy to build stream processing applications in many modern programming languages...Libraries such as Reactive Extensions, Akka Streams, or web frameworks such as React and Vue are all based on the idea of data streams that are connected to graphs to model the flow of data in applications. To the best of our knowledge, there exist no formalism which captures the essential core semantics of these approaches in a straightforward, easy to understand, manner: namely its graph-based program structure and the turn-based propagations of values through this graph. In this paper, we present Karcharias, a formalisation of reactive programming (a paradigm that shares many core ideas found in the various aforementioned libraries and frameworks) that is built from first principles. Instead of extending an existing language with a graph-based stream processing framework, and
formalising this integrated language, we formalised the reactive programming paradigm without relying on a base language (e.g., the λ-calculus). Using our formalism, we show how reactive programs (and thus, stream-based programs in general) need a way to construct a graph and to propagate events through that graph, even in the absence of a base language.