Higher-Order Mathematical Operational Semantics - Goncharov, Sergey; Milius, Stefan; Schröder, Lutz; Tsampas, Stylianos; Urbat, Henning (Leibniz International Proceedings in Informatics, LIPIcs, 2023)
We present a higher-order extension of Turi and Plotkin's abstract GSOS framework that retains the key feature of the latter: for every language whose operational rules are represented by a higher-order GSOS law, strong bisimilarity on the canonical operational model is a congruence with respect to the operations of the language. We further extend this result to weak (bi-)similarity, for which a categorical account of Howe's method is developed. It encompasses, for instance, Abramsky's classical compositionality theorem for applicative similarity in the untyped λ-calculus. In addition, we give first steps of a theory of logical relations at the level of higher-order abstract GSOS.
CRIS-Team Scopus Importer:2023-10-06
Keywords: Abstract GSOS; applicative bisimilarity; bialgebra; lambda-calculus