Logical Predicates in Higher-Order Mathematical Operational Semantics

2024/01/11 by Goncharov, Sergey, Santamaria, Alessio, Schröder, Lutz +2 · 3 citations
#FOS: Computer and information sciences #Logic in Computer Science (cs.LO) #Programming Languages (cs.PL)

paper · doi:10.48550/arxiv.2401.05872

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.

Cited by

• Higher-Order Behavioural Conformances via Fibrations
• Big Steps in Higher-Order Mathematical Operational Semantics
• Logical relations for call-by-push-value models, via internal fibrations in a 2-category

Related

• Weak Similarity in Higher-Order Mathematical Operational Semantics
• Open Higher-Order Logic (Long Version)
• A Categorical Integration of Logical Connectives via Higher Category Theory
• Embedding and Automating Conditional Logics in Classical Higher-Order Logic
• An Encoding of Abstract Dialectical Frameworks into Higher-Order Logic