Title: "Towards a Logic for Computational Effects"

Abstract:

In 1969 Dana Scott introduced LCF, his Logic for Computable Functions; 
its term language is a core higher-order call-by-name functional 
programming language with arithmetic, booleans and recursion at all 
types.  That lead to Milner et al's LCF system and then the programming 
language ML.  However, using this system to prove properties of programs
could not be done directly, requiring instead a translation to represent 
side-effects.  More recent, and very successful, program logics have yet 
another flavour, involving various modal and temporal logics.

We address the question as to whether there is a more uniform and 
general view.  To this end we follow an idea of Moggi that what is at 
kind is one or another notion of  *computational* effect, whether 
side-effects, nondeterminism or communication.  Other examples of 
computational effect are exceptions and probabilistic nondeterminism.

It turns out that all these different kinds of effects can be viewed 
algebraically, with the effects being generated by operations subject to 
natural equations.  Given that perspective, one can then give a (family 
of) of extensions of LCF (actually, call-by-value LCF) parameterised by 
the relevant computational effect.  Some standard temporal logics can be
directly represented as fragments of this logic.  Several real 
difficulties remain, particularly the representation of Hoare logics, 
but we do hope to have at least established the prospect of a unified view.