COOKIES: By using this website you agree that we can place Google Analytics Cookies on your device for performance monitoring. |

University of Cambridge > Talks.cam > Logic and Semantics Seminar (Computer Laboratory) > An algebraic theory of type-and-effect systems

## An algebraic theory of type-and-effect systemsAdd to your list(s) Download to your calendar using vCal - Ohad Kammar (University of Cambridge)
- Friday 13 December 2013, 13:00-14:00
- Room FW26, Computer Laboratory, William Gates Building.
If you have a question about this talk, please contact Jonathan Hayman. We present a theory of Gifford-style type-and-effect annotations, where effect annotations are sets of effects, such as memory accesses or exceptions. Our theory accounts for effect-dependent program transformations for functional-imperative languages, as used in optimising compilers. 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 observation is that annotation effects denote algebraic operations. After presenting our general type-and-effect system and its semantics, we validate and generalise existing optimisations and add new ones. Our 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 depend on the global nature of that theory, such as idempotency or absorption laws. We also give modularly-checkable necessary and sufficient conditions for validating the optimisations. Joint work with Gordon Plotkin. This talk is part of the Logic and Semantics Seminar (Computer Laboratory) series. ## This talk is included in these lists:- All Talks (aka the CURE list)
- Computer Laboratory talks
- Computing and Mathematics
- Logic and Semantics Seminar (Computer Laboratory)
- Room FW26, Computer Laboratory, William Gates Building
- School of Technology
Note that ex-directory lists are not shown. |
## Other listsCambridge University Polish Society Institute of Theoretical Geophysics Informal Lunchtime Seminars (DAMTP) Probability## Other talksIs the Era of Growth Miracles Over?” The gifts of Athena revisited: protectionism, regulation and the British Industrial Revolution, 1700–1800 Can deep, unsupervised models explain IT representations?/ Occluded object recognition in recurrent neural networks Complex Rays, Cones of Silence and Catastrophes Young people's science identities: A critique of the STEM pipeline Role of Adenovirus 36 in the Global Obesity Epidemic |