  We establish a general framework for reasoning about the relationship between
call-by-value and call-by-name.
  In languages with computational effects, call-by-value and call-by-name
executions of programs often have different, but related, observable
behaviours. For example, if a program might diverge but otherwise has no
effects, then whenever it terminates under call-by-value, it terminates with
the same result under call-by-name. We propose a technique for stating and
proving properties like these. The key ingredient is Levy's call-by-push-value
calculus, which we use as a framework for reasoning about evaluation orders. We
show that the call-by-value and call-by-name translations of expressions into
call-by-push-value have related observable behaviour under certain conditions
on computational effects, which we identify. We then use this fact to construct
maps between the call-by-value and call-by-name interpretations of types, and
identify further properties of effects that imply these maps form a Galois
connection. These properties hold for some computational effects (such as
divergence), but not others (such as mutable state). This gives rise to a
general reasoning principle that relates call-by-value and call-by-name. We
apply the reasoning principle to example computational effects including
divergence and nondeterminism.
