Making Reactive Programs Function

Add to your list(s) Download to your calendar using vCal

• Neel Krishnaswami, University of Cambridge
• Friday 09 September 2016, 14:00-15:00
• FW26.

If you have a question about this talk, please contact Dominic Mulligan.

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.

This talk is part of the Logic and Semantics Seminar (Computer Laboratory) series.

This talk is included in these lists:

• All Talks (aka the CURE list)
• Cambridge talks
• Computing and Mathematics
• Department of Computer Science and Technology talks and seminars
• FW26
• Interested Talks
• Logic and Semantics Seminar (Computer Laboratory)
• School of Technology
• Trust & Technology Initiative - interesting events
• bld31
• yk373's list

Note that ex-directory lists are not shown.