BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Talks.cam//talks.cam.ac.uk//
X-WR-CALNAME:Talks.cam
BEGIN:VEVENT
SUMMARY:Making Reactive Programs Function - Neel Krishnaswami\, University
  of Cambridge
DTSTART:20160909T130000Z
DTEND:20160909T140000Z
UID:TALK67158@talks.cam.ac.uk
CONTACT:Dominic Mulligan
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\, 
 they usually support full first-class general references\, which can conta
 in values of any type\, including higher types.  Concretely\, programmers 
 may store functions that can modify the heap\, within the heap itself.\n\n
 Since higher-order imperative programs are often much more difficult to un
 derstand than programs using either higher-order or imperative features al
 one\, programmers are encouraged to stick to the functional fragment much 
 as possible. However\, one place where higher-order state is used quite he
 avily in practice is in interactive programs\, like graphical user interfa
 ces.  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.\n\nIn this talk\
 , I will describe a recent line of work on structuring these kinds of prog
 rams\, 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 su
 rprises of this line of work is how many of the standard implementation te
 chniques for reactive programs turn out to realize fundamental logical pri
 mitives. This opens the door to reactive programming models which retain b
 oth the simple reasoning principles of functional programming\, and the ef
 ficient implementation strategies known to working programmers.
LOCATION:FW26
END:VEVENT
END:VCALENDAR