BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Talks.cam//talks.cam.ac.uk//
X-WR-CALNAME:Talks.cam
BEGIN:VEVENT
SUMMARY:Algebraic Foundations to Effect-Dependent Optimisations - Ohad Kam
 mar\, Edinburgh University
DTSTART:20120322T100000Z
DTEND:20120322T110000Z
UID:TALK37052@talks.cam.ac.uk
CONTACT:Microsoft Research Cambridge Talks Admins
DESCRIPTION:We present a general theory of Gifford-style type and effect a
 nnotations\, where effect annotations are sets of effects. Generality is a
 chieved by recourse to the theory of algebraic effects\, a development of 
 Moggi’s monadic theory of computational effects that emphasises the oper
 ations causing the effects at hand and their equational theory. The key ob
 servation is that annotation effects can be identified with operation symb
 ols.\n\nWe develop an annotated imperative and functional language with a 
 kind of computations for every effect set\; it can be thought of as a sequ
 ential\, annotated intermediate language. We develop a range of validated 
 optimisations (i.e.\, equivalences)\, generalising many existing ones and 
 adding new ones. We classify these optimisations as structural\, algebraic
 \, or abstract: structural optimisations always hold\; algebraic ones depe
 nd on the effect theory at hand\; and abstract ones depend on the global n
 ature of that theory (we give modularly-checkable sufficient conditions fo
 r their validity).\n\nJoint work with Gordon Plotkin\,  appeared in POPL'1
 2.\n
LOCATION:Large lecture theatre\, Microsoft Research Ltd\, 7 J J Thomson Av
 enue (Off Madingley Road)\, Cambridge
END:VEVENT
END:VCALENDAR