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.

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