Goncharov S, Milius S, Tsampas S, Urbat H (2024)
Publication Type: Conference contribution
Publication year: 2024
Publisher: Institute of Electrical and Electronics Engineers Inc.
Conference Proceedings Title: Proceedings - Symposium on Logic in Computer Science
Event location: Tallinn, EST
ISBN: 9798400706608
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 higherorder languages. Our main result states 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.
APA:
Goncharov, S., Milius, S., Tsampas, S., & Urbat, H. (2024). Bialgebraic Reasoning on Higher-order Program Equivalence. In Proceedings - Symposium on Logic in Computer Science. Tallinn, EST: Institute of Electrical and Electronics Engineers Inc..
MLA:
Goncharov, Sergey, et al. "Bialgebraic Reasoning on Higher-order Program Equivalence." Proceedings of the 39th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2024, Tallinn, EST Institute of Electrical and Electronics Engineers Inc., 2024.
BibTeX: Download