Weak Similarity in Higher-Order Mathematical Operational Semantics

Urbat H, Tsampas S, Goncharov S, Milius S, Schröder L (2023)


Publication Type: Conference contribution

Publication year: 2023

Journal

Publisher: Institute of Electrical and Electronics Engineers Inc.

Book Volume: 2023-June

Conference Proceedings Title: Proceedings - Symposium on Logic in Computer Science

Event location: Boston, MA, USA

ISBN: 9798350335873

DOI: 10.1109/LICS56636.2023.10175706

Abstract

Higher-order abstract GSOS is a recent extension of Turi and Plotkin's framework of Mathematical Operational Semantics to higher-order languages. The fundamental well-behavedness property of all specifications within the framework is that coalgebraic strong (bi)similarity on their operational model is a congruence. In the present work, we establish a corresponding congruence theorem for weak similarity, which is shown to instantiate to well-known concepts such as Abramsky's applicative similarity for the λ-calculus. On the way, we develop several techniques of independent interest at the level of abstract categories, including relation liftings of mixed-variance bifunctors and higher-order GSOS laws, as well as Howe's method.

Authors with CRIS profile

How to cite

APA:

Urbat, H., Tsampas, S., Goncharov, S., Milius, S., & Schröder, L. (2023). Weak Similarity in Higher-Order Mathematical Operational Semantics. In Proceedings - Symposium on Logic in Computer Science. Boston, MA, USA: Institute of Electrical and Electronics Engineers Inc..

MLA:

Urbat, Henning, et al. "Weak Similarity in Higher-Order Mathematical Operational Semantics." Proceedings of the 38th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2023, Boston, MA, USA Institute of Electrical and Electronics Engineers Inc., 2023.

BibTeX: Download