BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Talks.cam//talks.cam.ac.uk//
X-WR-CALNAME:Talks.cam
BEGIN:VEVENT
SUMMARY:An algebraic theory of type-and-effect systems - Ohad Kammar (Univ
 ersity of Cambridge)
DTSTART:20131213T130000Z
DTEND:20131213T140000Z
UID:TALK48973@talks.cam.ac.uk
CONTACT:Jonathan Hayman
DESCRIPTION:We present a theory of Gifford-style type-and-effect annotatio
 ns\, where effect annotations are sets of effects\, such as memory accesse
 s or exceptions. Our theory accounts for effect-dependent program transfor
 mations for functional-imperative languages\, as used in optimising compil
 ers. Generality is achieved by recourse to the theory of algebraic effects
 \, a development of Moggi’s monadic theory of computational effects that
  emphasises the operations causing the effects at hand. The key observatio
 n is that annotation effects denote algebraic operations. \n        \n    
     \nAfter presenting our general type-and-effect system and its semantic
 s\, we validate and generalise existing optimisations and add new ones. Ou
 r theory also suggests a classification of these optimisations into three 
 classes\, structural\, local\, and global: structural optimisations always
  hold\; local ones depend on the effect theory at hand\; and global ones d
 epend on the global nature of that theory\, such as idempotency or absorpt
 ion laws. We also give modularly-checkable necessary and sufficient condit
 ions for validating the optimisations.\n        \nJoint work with Gordon P
 lotkin.
LOCATION:Room FW26\, Computer Laboratory\, William Gates Building
END:VEVENT
END:VCALENDAR