BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//talks.cam.ac.uk//v3//EN
BEGIN:VTIMEZONE
TZID:Europe/London
BEGIN:DAYLIGHT
TZOFFSETFROM:+0000
TZOFFSETTO:+0100
TZNAME:BST
DTSTART:19700329T010000
RRULE:FREQ=YEARLY;BYMONTH=3;BYDAY=-1SU
END:DAYLIGHT
BEGIN:STANDARD
TZOFFSETFROM:+0100
TZOFFSETTO:+0000
TZNAME:GMT
DTSTART:19701025T020000
RRULE:FREQ=YEARLY;BYMONTH=10;BYDAY=-1SU
END:STANDARD
END:VTIMEZONE
BEGIN:VEVENT
CATEGORIES:Logic and Semantics Seminar (Computer Laboratory)
SUMMARY:Abstraction and Invariance for Algebraically Index
ed Types - Andrew Kennedy\, Microsoft Research Cam
bridge
DTSTART;TZID=Europe/London:20121109T140000
DTEND;TZID=Europe/London:20121109T150000
UID:TALK41162AThttp://talks.cam.ac.uk
URL:http://talks.cam.ac.uk/talk/index/41162
DESCRIPTION:The best way we know of describing the semantics o
f parametric polymorphism is relational parametric
ity\, whose central result is Reynolds' Abstractio
n Theorem. It has many striking consequences\, inc
luding "free theorems"\, non-inhabitation results\
, and encodings of\nalgebraic datatypes. \n\nRela
tional parametricity is a principle of invariance:
the behaviour of polymorphic code is invariant un
der changes of data representation. Invariance res
ults also abound in mathematics and physics. The a
rea of a triangle is invariant with respect to rot
ations and reflections\; the determinant of a matr
ix is invariant under changes of basis\; and Newto
n's laws are the same in all inertial frames.\n\nI
n this talk\, I will talk about recent work inspir
ed by this connection\, in which types are indexed
by attributes with algebraic structure\, and poly
morphism over such attributes expresses invariance
\nresults. I will describe in detail its applicati
on to computational geometry\, in which polymorphi
c types reflect that the behaviour of a program is
invariant under varieties of affine transformatio
n. This generalises earlier work on types for unit
s of measure. I will also describe applications to
information-flow security and continuity analysis
. \n\nThis is joint work with Robert Atkey and Pat
ricia Johann of the University of Strathclyde.
LOCATION:Room FW11\, Computer Laboratory\, William Gates Bu
ilding
CONTACT:Bjarki Holm
END:VEVENT
END:VCALENDAR