登录
站内检索:
[短期课程] Algebraic computational effects
[短期课程] Algebraic computational effects
2015-10-27
Title: Algebraic computational effects
Speaker: Professor Gordon Plotkin, University of Edinburgh
Schedule: October 26, 27: 10:00 - 12:00
                  October 29, 30: 10:00 - 12:00
Location: New Main Building G610, Beihang University
 
Abstract: Effects are central to programming languages, and include side-effects, exceptions, input, output, various forms of nondeterminism, nontermination, and continuations. A general theory of effects is therefore desirable. A first was provided by Eugenio Moggi who identified monads as providing a framework for modelling computational effects. Algebraic effects, first considered by John Power and myself, form a subclass where the effects can be modelled by bounded equational theories; the monads are then the corresponding free algebra monads. These effects include all the above examples other than continuations.
    The lectures begin with an account of this algebraic approach and how it fits in with Moggi's ideas; they then put the approach to work. The hope behind the algebraic approach is that many topics and applications, normally considered separately for individual effects, can instead be considered more or less uniformly for algebraic effects. As a first example, we will treat types and effect systems, providing an algebraic account of Wadler and Thiemanns’s indexed monads. As a second, we will consider effect handlers: whereas the algebraic operations can be considered as producing effects, handlers can be considered as consuming them. Applications are varied, ranging from exception handlers to parallelism. The lectures will come with exercises for the students. If implementation plans work out in time, Bauer and Pretnar’s Eff language, which is built around handlers, may also be available.
 
Lectures: 1. Algebraic effects I;
                 2. Type and effect systems;
                 3. Algebraic effects II;
                 4. Effect handlers.
 
Professor Gordon Plotkin is best known for his introduction of structural operational semantics and his work on denotational semantics. He was educated at the University of Glasgow and the University of Edinburgh, and has remained at Edinburgh, where he was a co-founder, with Rod Burstall, Matthew Hennessy, and Robin Milner, of the Laboratory for Foundations of Computer Science. He was elected a Fellow of the Royal Society in 1992. In 2012 he received the Royal Society's Milner Award.​