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:Microsoft Research Cambridge\, public talks
SUMMARY:Algebraic Foundations to Effect-Dependent Optimisa
tions - Ohad Kammar\, Edinburgh University
DTSTART;TZID=Europe/London:20120322T100000
DTEND;TZID=Europe/London:20120322T110000
UID:TALK37052AThttp://talks.cam.ac.uk
URL:http://talks.cam.ac.uk/talk/index/37052
DESCRIPTION:We present a general theory of Gifford-style type
and effect annotations\, where effect annotations
are sets of effects. Generality is achieved by rec
ourse to the theory of algebraic effects\, a devel
opment of Moggi’s monadic theory of computational
effects that emphasises the operations causing the
effects at hand and their equational theory. The
key observation is that annotation effects can be
identified with operation symbols.\n\nWe develop a
n annotated imperative and functional language wit
h a kind of computations for every effect set\; it
can be thought of as a sequential\, annotated int
ermediate language. We develop a range of validate
d optimisations (i.e.\, equivalences)\, generalisi
ng many existing ones and adding new ones. We clas
sify these optimisations as structural\, algebraic
\, or abstract: structural optimisations always ho
ld\; algebraic ones depend on the effect theory at
hand\; and abstract ones depend on the global nat
ure of that theory (we give modularly-checkable su
fficient conditions for their validity).\n\nJoint
work with Gordon Plotkin\, appeared in POPL'12.\n
LOCATION:Large lecture theatre\, Microsoft Research Ltd\, 7
J J Thomson Avenue (Off Madingley Road)\, Cambrid
ge
CONTACT:Microsoft Research Cambridge Talks Admins
END:VEVENT
END:VCALENDAR