Bialgebraic Reasoning on Higher-order Program Equivalence

FOS: Computer and information sciences Computer Science - Logic in Computer Science Computer Science - Programming Languages 0102 computer and information sciences 01 natural sciences Logic in Computer Science (cs.LO) Programming Languages (cs.PL)
DOI: 10.1145/3661814.3662099 Publication Date: 2024-06-21T12:30:12Z
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 $λ$-calculi with recursive types, and to different flavours of contextual equivalence.
SUPPLEMENTAL MATERIAL
Coming soon ....
REFERENCES (85)
CITATIONS (1)
EXTERNAL LINKS
PlumX Metrics
RECOMMENDATIONS
FAIR ASSESSMENT
Coming soon ....
JUPYTER LAB
Coming soon ....