BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Talks.cam//talks.cam.ac.uk//
X-WR-CALNAME:Talks.cam
BEGIN:VEVENT
SUMMARY:Causality for Free!  Parametricity Implies Causality for Functiona
 l Reactive Programs - Alan Jeffrey\, Bell Labs
DTSTART:20120723T130000Z
DTEND:20120723T143000Z
UID:TALK39064@talks.cam.ac.uk
CONTACT:Microsoft Research Cambridge Talks Admins
DESCRIPTION:Functional Reactive Programming (FRP) is a model of reactive s
 ystems in which signals are time-dependent values\, and signal functions a
 re functions between signals. Signal functions are required to be causal\,
  in that output behaviour at time t is only allowed to depend on input beh
 aviour up to time t. In order to enforce causality\, many FRP libraries ar
 e arrowized\, in that they provide combinators for building signal functio
 ns\, rather than allowing users to write functions directly. In this paper
 \, we provide a definition of deep causality (which coincides with the usu
 al definition on signals of base type\, but differs on nested signals). We
  show that FRP types can be interpreted in System Fω extended with a kind
  of time\, and show that in this interpretation\, a “theorems for free
 ” argument shows that parametric functions are deep causal. Since all Sy
 stem Fω functions are parametric\, this implies that all implementable fu
 nctions are deep causal. This model is the formal basis of the agda-frp-js
  FRP library for the dependently typed programming language Agda\, which c
 ompiles to JavaScript and executes in the browser. Assuming parametricity 
 of Agda\, this allows reactive programs to be written as regular functions
  over signals\, without sacrificing causality. All results have been mecha
 nically verified in Agda.
LOCATION:Small lecture theatre\, Microsoft Research Ltd\, 7 J J Thomson Av
 enue (Off Madingley Road)\, Cambridge
END:VEVENT
END:VCALENDAR