Effects and Call-By-Push-Value

Paul Blain Levy, University of Birmingham

This course is an introduction to call-by-push-value, a fine-grained calculus that subsumes both call-by-value and call-by-name lambda-calculus with computational effects (imperative features).

After introducing the language, and the translations from call-by-value and call-by-name, we'll learn both operational and denotational semantics for a variety of effects: exceptions, I/O, state and control (continuations).

This course is aimed at students with knowledge of typed lambda-calculus. I encourage students to read my course notes on typed lambda-calculus, at least up to Section 14, before the course. I will recap in the first lecture but rather quickly.

Here are the course slides and some exercises.