一句话：用 call-by-push-value 与 Galois 连接刻画传值与传名的可观察行为关系。
论文研究带计算效应的语言中 call-by-value 与 call-by-name 执行的可观察行为关系。作者以 Levy 的 call-by-push-value 演算为统一框架，将表达式分别翻译为传值与传名解释，并识别使两者行为相关的效应条件。基于这些条件，他们在类型的传值与传名解释之间构造映射，并给出效应应满足的额外性质，使这些映射构成 Galois 连接。该性质对发散等效应成立，但对可变状态等效应不成立，从而得到一个通用的推理原则。作者将该原则应用于发散与非确定性等计算效应，说明何时可从一种求值策略的终止或结果推断另一种策略。
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.