一句话：将差分逻辑关系推广到带效应高阶程序，用 quantale 度量值与计算效应之间的距离。
传统语义学关注程序等价，不等价程序通常被视为不可比较。近年出现的程序度量用 quantale 元素衡量不等价程序间的距离，而差分逻辑关系通过随类型复杂度改变底层 quantale，实现上下文敏感的推理。本文把这一框架推广到带效应的高阶程序，不仅对返回值，而且对计算产生的效应也进行有原则的距离化。作者表明该框架具有灵活性，能处理多种形式的效应，并能给出关于程序差异的简洁且信息丰富的判断。
Semantics is traditionally concerned with program equivalence, in which all pairs of programs which are not equivalent are treated the same, and simply dubbed as incomparable. In recent years, various forms of program metrics have been introduced such that the distance between non-equivalent programs is measured as an element of an appropriate quantale. By letting the underlying quantale vary as the type of the compared programs become more complex, the recently introduced framework of differential logical relations allows for a new contextual form of reasoning. In this paper, we show that all this can be generalised to effectful higher-order programs, in which not only the values , but also the effects computations produce can be appropriately distanced in a principled way. We show that the resulting framework is flexible, allowing various forms of effects to be handled, and that it provides compact and informative judgments about program differences.