Making Reactive Programs Function

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

• Dr Neel Krishnaswami - University of Cambridge, Computer Laboratory
• Wednesday 23 November 2016, 16:15-17:15
• Lecture Theatre 2, Computer Laboratory.

If you have a question about this talk, please contact David Greaves.

Note: Venue is LT2 (not LT1).

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 Wednesday Seminars - Department of Computer Science and Technology series.

This talk is included in these lists:

• All Talks (aka the CURE list)
• Cambridge Centre for Data-Driven Discovery (C2D3)
• Cambridge talks
• Chris Davis' list
• Department of Computer Science and Technology talks and seminars
• Graduate-Seminars
• Guy Emerson's list
• Interested Talks
• Lecture Theatre 2, Computer Laboratory
• School of Technology
• Trust & Technology Initiative - interesting events
• Wednesday Seminars - Department of Computer Science and Technology
• bld31
• computer science
• ndk22's list
• ob366-ai4er
• rp587
• se393's list

Note that ex-directory lists are not shown.