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.

• Type: Conference
• Year: 2003
• Where: IWFM
• Authors: Gordon D. Plotkin, John Power
• Keywords: Computational Effects, Formal Methods, IWFM 2003, Logic, Possible Logic