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.
|