What happens when we try to extend typed lambda-calculus (i.e. pure functional programming) with computational effects (i.e. imperative features)? It initially seems that we must choose between call-by-value (CBV) and call-by-name (CBN) evaluation. However, semantic analysis reveals a single calculus that subsumes both options. Known as call-by-push-value (CBPV), it is based on the slogan “A value is, a computation does”.
This talk introduces CBPV and the decomposition of CBV/CBN typed lambda-calculus into it.