BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Talks.cam//talks.cam.ac.uk//
X-WR-CALNAME:Talks.cam
BEGIN:VEVENT
SUMMARY:Abstraction and Invariance for Algebraically Indexed Types - Andre
 w Kennedy\, Microsoft Research Cambridge
DTSTART:20121109T140000Z
DTEND:20121109T150000Z
UID:TALK41162@talks.cam.ac.uk
CONTACT:Bjarki Holm
DESCRIPTION:The best way we know of describing the semantics of parametric
  polymorphism is relational parametricity\, whose central result is Reynol
 ds' Abstraction Theorem. It has many striking consequences\, including "fr
 ee theorems"\, non-inhabitation results\, and encodings of\nalgebraic data
 types.  \n\nRelational parametricity is a principle of invariance: the beh
 aviour of polymorphic code is invariant under changes of data representati
 on. Invariance results also abound in mathematics and physics. The area of
  a triangle is invariant with respect to rotations and reflections\; the d
 eterminant of a matrix is invariant under changes of basis\; and Newton's 
 laws are the same in all inertial frames.\n\nIn this talk\, I will talk ab
 out recent work inspired by this connection\, in which types are indexed b
 y attributes with algebraic structure\, and polymorphism over such attribu
 tes expresses invariance\nresults. I will describe in detail its applicati
 on to computational geometry\, in which polymorphic types reflect that the
  behaviour of a program is invariant under varieties of affine transformat
 ion. This generalises earlier work on types for units of measure. I will a
 lso describe applications to information-flow security and continuity anal
 ysis. \n\nThis is joint work with Robert Atkey and Patricia Johann of the 
 University of Strathclyde.
LOCATION:Room FW11\, Computer Laboratory\, William Gates Building
END:VEVENT
END:VCALENDAR