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.