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.

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