Logical Predicates in Higher-Order Mathematical Operational Semantics
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.
Cite
@article{arxiv.2401.05872,
title = {Logical Predicates in Higher-Order Mathematical Operational Semantics},
author = {Sergey Goncharov and Alessio Santamaria and Lutz Schröder and Stelios Tsampas and Henning Urbat},
journal= {arXiv preprint arXiv:2401.05872},
year = {2024}
}
Comments
Extended version