Logic for Computational Effects work in progress - BCS.pdfVIP

1 Logic for Computational Effects: work in progress Gordon Plotkin and John Power School of Informatics University of Edinburgh King’s Buildings Mayfield Road Edinburgh EH9 3JZ Scotland gdp@inf.ed.ac.uk, ajp@inf.ed.ac.uk 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. Keywords: Computational effects, computational λ-calculus, signature, operations, equations, modalities, F reyd-categories. 1. INTRODUCTION We are attempting to develop a formal logical system for reasoning about computational effects in a unified manner. Our starting point is Eugenio Moggi’s computational λ-calculus or λ - c calculus [5, 6]. The λ -calculus terms provide an underlying call-by-value functional