Reactive Programming

  • Mezzalira L
N/ACitations
Citations of this article
14Readers
Mendeley users who have this article in their library.
Get full text

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.

Cite

CITATION STYLE

APA

Mezzalira, L. (2018). Reactive Programming. In Front-End Reactive Architectures (pp. 65–96). Apress. https://doi.org/10.1007/978-1-4842-3180-7_3

Register to see more suggestions

Mendeley helps you to discover research relevant for your work.

Already have an account?

Save time finding and organizing research with Mendeley

Sign up for free