Logical relations built on top of an operational semantics are one of the most successful proof methods in programming language semantics. In recent years, more and more expressive notions of operationally-based logical relations have been designed and applied to specific families of languages. However, a unifying abstract framework for operationally-based logical relations is still missing. We show how fibrations can provide a uniform treatment of operational logical relations, using as reference example a lambda-calculus with generic effects endowed with a novel, abstract operational semantics defined on a large class of categories. Moreover, this abstract perspective allows us to give a solid mathematical ground also to differential logical relations -- a recently introduced notion of higher-order distance between programs -- both pure and effectful, bringing them back to a common picture with traditional ones.

翻译：基于操作语义构建的逻辑关系是编程语言语义学中最成功的证明方法之一。近年来，越来越多表达力更强的基于操作的逻辑关系概念被设计出来，并应用于特定语言族系。然而，目前仍缺乏一个统一的基于操作的逻辑关系的抽象框架。我们展示了纤维化如何为操作逻辑关系提供统一处理，并以带有泛型效应的λ演算为参考示例，该演算采用了一种新颖的、定义在广泛范畴类上的抽象操作语义。此外，这种抽象视角使我们能够为微分逻辑关系（一种最近引入的程序间高阶距离概念）提供坚实的数学基础——无论是纯的还是带效应的，并将它们与传统的逻辑关系统一到同一图景中。