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.

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