| Edinburgh EH9 3JZ Scotland (2007) | |||||||||||||||
Abstract | |||||||||||||||
| We outline a possible logic that will allow us to give a unied approach to reasoning about computational eects. 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 eects, and we observe that operations give rise to natural modalities. 1 | |||||||||||||||
Publication details | |||||||||||||||
| |||||||||||||||