A modular approach to denotational semantics

Abstract

We give an account of part of modularity in denotational semantics. We define a computational effect to consist of a category with algebraic structure together with a construction using that algebraic structure of a new denotational category together with an identity on objects functor to it from the original category. We make precise what we mean by algebraic structure and what constructions are allowable. Further, given two computational effects, we give a mathematical foundation for extending one along the other. We prove a theorem to show when such a extension is possible.