Bialgebraic Reasoning on Higher-order Program Equivalence

• DOI: 10.1145/3661814.3662099
• Publication Date: 2024-06-21T12:30:12Z
• Authors: Sergey Goncharov; Stefan Milius; Stelios Tsampas; Henning Urbat
• Keywords: FOS: Computer and information sciences; Computer Science - Logic in Computer Science; Computer Science - Programming Languages; 0202 electrical engineering, electronic engineering, information engineering; 0102 computer and information sciences; Logic in Computer Science (cs.LO); Programming Languages (cs.PL)

Logical relations constitute a key method for reasoning about contextual equivalence of programs in higher-order languages. They are usually developed on a per-case basis, with a new theory required for each variation of the language or of the desired notion of equivalence. In the present paper we introduce a general construction of (step-indexed) logical relations at the level of Higher-Order Mathematical Operational Semantics, a highly parametric categorical framework for modeling the operational semantics of higher-order languages. Our main result asserts that for languages whose weak operational model forms a lax bialgebra, the logical relation is automatically sound for contextual equivalence. Our abstract theory is shown to instantiate to combinatory logics and $λ$-calculi with recursive types, and to different flavours of contextual equivalence.