Algebraic Foundations for Type and Effect Analysis

Add to your list(s) Download to your calendar using vCal

• Ohad Kammar, University of Edinburgh
• Thursday 23 June 2011, 14:00-15:00
• UG40 Computer Science.

If you have a question about this talk, please contact Paul Levy.

We propose a semantic foundation for optimisations based on type and effect analysis. We present a multiple-effect call-by-push-value based calculus whose denotational semantics is based on an effect-indexed structure of adjunctions. When the underlying set of effects is specified by an algebraic theory, we take effects to be given by sets of operations. The required adjunction structure can then be obtained via a uniform process of conservative restriction of the theory. The modular composition of effects then boils down to extension conservativeness results.

We use our calculus and its semantics to provide general effect- dependent optimisations. Many of the already known effect-dependent optimisations are then particular cases of our general ones. We have thus demonstrated the possibility of a general theory of effect optimisations based on the algebraic theory of effects.

(Joint work with Gordon Plotkin)

This talk is part of the Theoretical computer science seminar series.

This talk is included in these lists:

• Computer Science Departmental Series
• Computer Science Distinguished Seminars
• Theoretical computer science seminar
• UG40 Computer Science
• computer sience

Note that ex-directory lists are not shown.