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.