Paul Levy
University of
Birmingham
Abstract:
Call-by-push-value
is a calculus for computational effects that provides fine-grain
primitives into which both call-by-value and call-by-name calculi can
be decomposed. This decomposition appears in a wide variety of
semantics: operational, domains, state, continuations, games, possible
worlds, etc.
We first look at semantics of call-by-value and call-by-name, using
algebras for a monad, and see how that leads us to call-by-push-value.
We then look at two examples of call-by-push-value semantics that do
not use algebras: state (global ground) and continuations.
Wednesday, June 18, 2008
3:30 p.m.
Wean
Hall 8220
Principles
of Programming Seminars