Abstract

The ML family of programming languages is best known as a family of functional programming languages, but most ML-family languages also offer support for effects such as control operators and state. Indeed, they usually support full first-class general references, which can contain values of any type, including higher types. Concretely, programmers may store functions that can modify the heap, within the heap itself.

Since higher-order imperative programs are often much more difficult to understand than programs using either higher-order or imperative features alone, programmers are encouraged to stick to the functional fragment much as possible. However, one place where higher-order state is used quite heavily in practice is in interactive programs, like graphical user interfaces. These reactive systems are typically implemented in an aggressively higher-order stateful style, with each mutable component storing a set of callbacks to invoke whenever a particular event happens.

In this talk, I will describe a recent line of work on structuring these kinds of programs, based on the idea of using a Curry-Howard proof term correspondence with temporal logic as a type system for reactive programs. One of the surprises of this line of work is how many of the standard implementation techniques for reactive programs turn out to realize fundamental logical primitives. This opens the door to reactive programming models which retain both the simple reasoning principles of functional programming, and the efficient implementation strategies known to working programmers.