Wednesday 16th March, 2005

An Algebraic Theory of Computational Effects
presented by Gordon Plotkin

Logic and computer science interact in a variety of ways. In the context of programming languages, the Curry-Howard correspondence leads to a well-known relation between proof theory and functional programming. However there is more to understand if we are to have a satisfactory "logical reconstruction" of programming languages. One ingredient concerns the treatment of computational effects, such as: exceptions, side-effects, interactive input/output, and probabilistic and ordinary nondeterminism. We discuss how these might be treated logically using ideas from (suitably generalised) equational logic and category theory.


Last modified Feb 3rd, 2005
Maintained by Pat Hill (hill@comp.leeds.ac.uk)