References & Citations
Computer Science > Logic in Computer Science
Title: Bialgebraic Reasoning on Higher-Order Program Equivalence
(Submitted on 1 Feb 2024 (v1), last revised 16 May 2024 (this version, v2))
Abstract: 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 $\lambda$-calculi with recursive types, and to different flavours of contextual equivalence.
Submission history
From: Stelios Tsampas [view email][v1] Thu, 1 Feb 2024 14:40:17 GMT (177kb)
[v2] Thu, 16 May 2024 14:28:13 GMT (203kb)
Link back to: arXiv, form interface, contact.