# Higher-Order Functional Reactive Programming

## Neelakantan Krishnaswami (Birmingham)

While functional programming languages such as Ocaml and Haskell have
demonstrated that many programming tasks lend themselves to simple and
elegant formulations in terms of functional programming, interactive
programs have proven surprisingly resistant to being cast in a
functional style.

In this course, I will survey some recent progress on this
problem, based on the striking observation that it is possible
to give types to reactive programs using formulas of temporal
logic.

From the perspective of proof theory, this leads to a Curry-
Howard proof term assignment for constructive temporal logic.
From the view of programming, interactive programs can be written
as surprisingly simple functional programs. From the perspective
of implementation, the type discipline lends itself to simple and
efficient implementation strategies. Finally, these type systems
shed new light on powerful techniques like step-indexing.

Last modified: Wed Jan 22 16:25:41 GMT 2014