University of Cambridge > Talks.cam > Logic and Semantics Seminar (Computer Laboratory) > Making Reactive Programs Function

Making Reactive Programs Function

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

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.

Tell a friend about this talk:

This talk is included in these lists:

Note that ex-directory lists are not shown.

 

© 2006-2024 Talks.cam, University of Cambridge. Contact Us | Help and Documentation | Privacy and Publicity