Reactive Programming

Abstract

Functional Reactive Programming (FRP) models reactive systems with events and signals, which have previously been observed to correspond to the “eventually” and “always” modalities of linear temporal logic (LTL). In this paper, we define a constructive vari- ant of LTL with least fixed point and greatest fixed point opera- tors in the spirit of the modal mu-calculus, and give it a proofs-as- programs interpretation as a foundational calculus for reactive programs. Previous work emphasized the propositions-as-types part of the correspondence between LTL and FRP; here we emphasize the proofs-as-programs part by employing structural proof theory. We show that the type system is expressive enough to enforce liveness properties such as the fairness of schedulers and the eventual de- livery of results. We illustrate programming in this calculus using (co)iteration operators. We prove type preservation of our opera- tional semantics, which guarantees that our programs are causal. We give also a proof of strong normalization which provides justi- fication that our programs are productive and that they satisfy liveness properties derived from their types.