Functional reactive programming (FRP) is an elegant approach to declaratively specify reactive systems. However, the powerful abstractions of FRP have historically made it difficult to predict and control the resource usage of programs written in this style.

In this talk, I describe a new language for higher-order reactive programming. This language generalizes and simplifies work on functional reactive programming, supporting the use of higher-order abstractions such as first-class functions and streams of streams.

Furthermore, the type system can be understood (via the Curry-Howard correspondence) as a proof system for a variant of linear temporal logic, and the type discipline also permits a simple and provably efficient implementation strategy.

Time permitting, I will also discuss some preliminary work on denotational models for this calculus.