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.