Interpreting localized computational effects using operators of higher type

Abstract

We outline a general approach to providing intensional models for languages with computational effects, whereby the problem of interpreting a given effect reduces to that of finding an operator of higher type satisfying certain equations. Our treatment consolidates and generalizes an idea that is already implicit in the literature on game semantics. As an example, we work out our approach in detail for the case of fresh name generation, and discuss some particular models to which it applies. © 2008 Springer-Verlag Berlin Heidelberg.