We add, one at a time, 3 computational effects:
We carefully establish denotational semantics for each of these 6 languages, proving soundness in each case. For call-by-value, we look at the fine-grain call-by-value language which simplifies the semantics. For call-by-name, we move from carrier semantics (suitable for divergence) to algebra semantics (suitable for printing) to behaviour semantics (suitable for storage).
We arrange these semantics in a table and spot the pattern: it is evident that there is a single language underlying call-by-value and call-by-name. This language is call-by-push-value, and we discuss its basic properties.