Bialgebraic Reasoning on Higher-Order Program Equivalence
CoRR(2024)
摘要
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.
更多查看译文
AI 理解论文
溯源树
样例
生成溯源树,研究论文发展脉络
Chat Paper
正在生成论文摘要