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.

This distinguished lecture is held in honor of Dana Scott's impending retirement. Plotkin has been for more than two decades the leading researcher in the theory of programming languages. Much of his work has been deeply influenced by Scott's invention of domain theory as a comprehensive framework for the semantics of programming languages. Plotkin's work has been especially influential in establishing deep connections between domain theory, category theory, and type theory, all of which are of great importance in contemporary programming language research. He has also made important contributions in automatic theorem proving, most recently through his work on the LF logical framework. It is a great honor for the School, and a fitting tribute to Dana's career, to have Plotkin as this year's final distinguished lecturer.

Speaker Bio:

Gordon Plotkin is Professor of Theoretical Computer Science at the University of Edinburgh, He is a co-founder of the Laboratory for the Foundations of Computer Science (LFCS) and a Fellow of the Royal Society. He has contributed to the development of the denotational and operational semantics of programming languages and related mathematical and logical topics. His current interests include the algebraic theory of computational effects and computational systems biology.

<< Back