Higher-order Abstract GSOS

Summary

Higher-order Abstract GSOS (HO-GSOS), also known as Higher-order Mathematical Operational Semantics, is a novel categorical framework to develop, implement and study the properties of higher-order programming languages.

Our framework extends the original, first-order counterpart of (first-order) Abstract GSOS introduced by Turi and Plotkin in their seminal 1997 paper Towards a Mathematical Operational Semantics [1]. In it, Turi and Plotkin present a conceptual realization of operational semantics as certain kinds of distributive laws (natural transformations) in a suitable category, in effect giving programming languages a generic, mathematical definition. There two main advantages attributed to Abstract GSOS: first, distributive laws are especially precise when it comes to the modelling of certain classes of first-order systems such as (first-order) process calculi. Second, bisimilarity for languages expressed in Abstract GSOS is automatically a congruence, a fundamental well-behavedness property that is typically hard to prove.

By far, the most crucial limitation of Abstract GSOS was its inability to model higher-order systems such as the \(\lambda\)-calculus. In early 2023 [2], a number of researchers from the Theoretical Computer Science group at FAU Erlangen-Nürnberg, which included myself, managed to finally extend Abstract GSOS to the higher-order setting, thus initiating the research programme on Higher-order Abstract GSOS.

Publications on HO-GSOS

• Abstract Operational Methods for Call-by-Push-Value, POPL’25 [3]
• Bialgebraic Reasoning on Higher-Order Program Equivalence, LICS’24 [4]
• Logical Predicates in Higher-Order Mathematical Operational Semantics, FoSSaCS’24 [5]
• Weak Similarity in Higher-Order Mathematical Operational Semantics, LICS’23 [6]
• Towards a Higher-Order Mathematical Operational Semantics, POPL’23 [2]

Project Outline

Since the beginning of the HO-GSOS project in 2023 with its intruduction in Gocharov et al. [2], there has been important progress in a variety of fronts, such as implementing Logical Relations and Howe’s method ([4], [5], [6]). However, the vast majority of the work is ahead of us. We can divide this future work, and by extension the future of HO-GSOS, in four main categories:

• Programming paradigms, i.e. supporting the various diverse classes of languages.
• Reasoning methodologies, i.e. developing more methods to reason about program correctness.
• Secure compilation, i.e. developing a theory on secure/verified compilation.
• Mechanization/implementation, i.e. developing verification tools based on HO-GSOS.

The following diagram provides an overview of the completed work and our future plans on HO-HSOS.