Logical Predicates in Higher-Order Mathematical Operational Semantics
Sergey Goncharov, Alessio Santamaria, Lutz Schröder, Stelios Tsampas, Henning Urbat
TL;DR
The paper advances a unifying coalgebraic theory of operational logical relations for higher‑order languages by modeling languages as higher‑order GSOS laws and treating logical predicates as invariant coalgebraic properties with predicate liftings. It introduces locally maximal logical refinements $\square P$ and induction‑up‑to techniques that enable concise proofs for complex properties (e.g., strong normalization) across whole families of languages under relatively flat higher‑order GSOS laws. Concrete instantiations include strong normalization for typed combinatory logic and type safety for STLC, and the framework is shown to generalize to higher‑order languages via a parametric, modular approach. The results promise a scalable, generic methodology for reasoning about contextual equivalence and other semantic properties in higher‑order, possibly effectful, languages.
Abstract
We present a systematic approach to logical predicates based on universal coalgebra and higher-order abstract GSOS, thus making a first step towards a unifying theory of logical relations. We first observe that logical predicates are special cases of coalgebraic invariants on mixed-variance functors. We then introduce the notion of a locally maximal logical refinement of a given predicate, with a view to enabling inductive reasoning, and identify sufficient conditions on the overall setup in which locally maximal logical refinements canonically exist. Finally, we develop induction-up-to techniques that simplify inductive proofs via logical predicates on systems encoded as (certain classes of) higher-order GSOS laws by identifying and abstracting away from their boiler-plate part.