## Effects and Call-By-Push-Value

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.

Course slides.

Exercises for Monday's lectures