Text size
  • Small
  • Medium
  • Large
  • Standard
  • Blue text on blue
  • High contrast (Yellow text on black)
  • Blue text on beige

    Logic for Computational Effects: Work in Progress

    6th International Workshop on Formal Methods

    Dublin City University, Ireland. 11 July, 2003


    Gordon Plotkin & John Power


    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.


    PDF filePDF Version of this Paper (54kb)