University of Birmingham > Talks@bham > Theoretical computer science seminar > Algebraic Foundations for Type and Effect Analysis

Algebraic Foundations for Type and Effect Analysis

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

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.

Tell a friend about this talk:

This talk is included in these lists:

Note that ex-directory lists are not shown.


Talks@bham, University of Birmingham. Contact Us | Help and Documentation | Privacy and Publicity.
talks@bham is based on from the University of Cambridge.