Logic for Computational Effects: work in progress

We outline a possible logic that will allow us to give a unified approach to reasoning about computational effects. The logic is given by extending Moggi’s computational λcalculus by basic types and a signature, the latter given by constant symbols, function symbols, and operation symbols, and by including a μ operator. We give both syntax and semantics for the logic except for λ. We consider a number of sound and complete classes of models, all given in category-theoretic terms. We illustrate the ideas with some of our leading examples of computational effects, and we observe that operations give rise to natural modalities.