| Logic for Computational Effects: work in progress (2008) | |||||||||||||||
Abstract | |||||||||||||||
| Abstract 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. | |||||||||||||||
Publication details | |||||||||||||||
| |||||||||||||||