BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Talks.cam//talks.cam.ac.uk//
X-WR-CALNAME:Talks.cam
BEGIN:VEVENT
SUMMARY:Making Reactive Programs Function - Dr Neel Krishnaswami - Univers
 ity of Cambridge\, Computer Laboratory
DTSTART:20161123T161500Z
DTEND:20161123T171500Z
UID:TALK67811@talks.cam.ac.uk
CONTACT:David Greaves
DESCRIPTION:The ML family of programming languages is best known as a fami
 ly of functional programming languages\, but most ML-family languages also
  offer support for effects such as control operators and state. Indeed\, t
 hey usually support full first-class general references\, which can contai
 n values of any type\, including higher types. Concretely\, programmers ma
 y store functions that can modify the heap\, within the heap itself.\n\nSi
 nce higher-order imperative programs are often much more difficult to unde
 rstand than programs using either higher-order or imperative features alon
 e\, programmers are encouraged to stick to the functional fragment much as
  possible. However\, one place where higher-order state is used quite heav
 ily in practice is in interactive programs\, like graphical user interface
 s. These reactive systems are typically implemented in an aggressively hig
 her-order stateful style\, with each mutable component storing a set of ca
 llbacks to invoke whenever a particular event happens.\n\nIn this talk\, I
  will describe a recent line of work on structuring these kinds of program
 s\, based on the idea of using a Curry-Howard proof term correspondence wi
 th temporal logic as a type system for reactive programs. One of the surpr
 ises of this line of work is how many of the standard implementation techn
 iques for reactive programs turn out to realize fundamental logical primit
 ives. This opens the door to reactive programming models which retain both
  the simple reasoning principles of functional programming\, and the effic
 ient implementation strategies known to working programmers.\n
LOCATION:Lecture Theatre 2\, Computer Laboratory
END:VEVENT
END:VCALENDAR
