A categorical framework of higher-order programming languages.
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
Higher-Order Bialgebraic Semantics, J. Funct. Program.[3]
Higher-Order Behavioural Conformances via Fibrations, POPL’26[4]
Bialgebraic Reasoning on Stateful Languages, ICFP’25[5]
Big Steps in Higher-Order Mathematical Operational Semantics, ICFP’25[6]
Abstract Operational Methods for Call-by-Push-Value, POPL’25[7]
Bialgebraic Reasoning on Higher-Order Program Equivalence, LICS’24[8]
Logical Predicates in Higher-Order Mathematical Operational Semantics, FoSSaCS’24[9]
Weak Similarity in Higher-Order Mathematical Operational Semantics, LICS’23[10]
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
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.
Overview of the Higher-order Abstract GSOS project.
References
2026
J. Funct. Program.
Higher-Order Bialgebraic Semantics
Sergey Goncharov, Stefan Milius, Lutz Schröder, Stelios Tsampas, and Henning Urbat
Journal of Functional Programming, 2026
POPL
Higher-Order Behavioural Conformances via Fibrations
Coinduction is a widely used technique for establishing behavioural equivalence of programs in higher-order languages. In recent years, the rise of languages with quantitative (e.g. probabilistic) features has led to extensions of coinductive methods to more refined types of behavioural conformances, most notably notions of behavioural distance. To guarantee soundness of coinductive reasoning, one needs to show that the behavioural conformance at hand forms a program congruence, i.e. it is suitably compatible with the operations of the language. This is usually achieved by a complex proof technique known as Howe’s method, which needs to be carefully adapted to both the specific language and the targeted notion of behavioural conformance. We develop a uniform categorical approach to Howe’s method that features two orthogonal dimensions of abstraction: (1) the underlying higher-order language is modelled by an abstract higher-order specification (AHOS), a novel and very general categorical account of operational semantics, and (2) notions of behavioural conformance (such as relations or metrics) are modelled via fibrations over the base category of an AHOS. Our main result is a fundamental congruence theorem at this level of generality: Under natural conditions on the categorical ingredients and the operational rules of a language modelled by an AHOS, the greatest behavioural (bi)conformance on its operational model forms a congruence. We illustrate our theory by deriving congruence of bisimilarity and behavioural pseudometrics for probabilistic higher-order languages.
2025
ICFP
Bialgebraic Reasoning on Stateful Languages
Sergey Goncharov, Stefan Milius, Lutz Schröder, Stelios Tsampas, and Henning Urbat
Reasoning about program equivalence in imperative languages is notoriously challenging, as the presence of states (in the form of variable stores) fundamentally increases the observational power of program terms. The key desideratum for any notion of equivalence is compositionality, guaranteeing that subprograms can be safely replaced by equivalent subprograms regardless of the context. To facilitate compositionality proofs and avoid boilerplate work, one would hope to employ the abstract bialgebraic methods provided by Turi and Plotkin’s powerful theory of mathematical operational semantics (a.k.a. abstract GSOS) or its recent extension by Goncharov et al. to higher-order languages. However, multiple attempts to apply abstract GSOS to stateful languages have thus failed. We propose a novel approach to the operational semantics of stateful languages based on the formal distinction between readers (terms that expect an initial input store before being executed), and writers (running terms that have already been provided with a store). In contrast to earlier work, this style of semantics is fully compatible with abstract GSOS, and we can thus leverage the existing theory to obtain coinductive reasoning techniques. We demonstrate that our approach generates non-trivial compositionality results for stateful languages with first-order and higher-order store and that it flexibly applies to program equivalences at different levels of granularity, such as trace, cost, and natural equivalence.
ICFP
Big Steps in Higher-Order Mathematical Operational Semantics
Sergey Goncharov, Pouya Partow, and Stelios Tsampas
Small-step and big-step operational semantics are two fundamental styles of structural operational semantics (SOS), extensively used in practice. The former one is more fine-grained and is usually regarded as primitive, as it only defines a one-step reduction relation between a given program and its direct descendant under an ambient evaluation strategy. The latter one implements, in a self-contained manner, such a strategy directly by relating a program to the net result of the evaluation process. The agreement between these two styles of semantics is one of the key pillars in operational reasoning on programs; however, such agreement is typically proven from scratch every time on a case-by-case basis. A general, abstract mathematical argument behind this agreement is up till now missing. We cope with this issue within the framework of higher-order mathematical operational semantics by providing an abstract categorical notion of big-step SOS, complementing the existing notion of abstract higher-order GSOS. Moreover, we introduce a general construction for deriving the former from the latter, and prove an abstract equivalence result between the two.
POPL
Abstract Operational Methods for Call-by-Push-Value
Sergey Goncharov, Stelios Tsampas, and Henning Urbat
Levy’s call-by-push-value is a comprehensive programming paradigm that combines elements from functional and imperative programming, supports computational effects and subsumes both call-by-value and call-by-name evaluation strategies. In the present work, we develop modular methods to reason about program equivalence in call-by-push-value, and in fine-grain call-by-value, which is a popular lightweight call-by-value sublanguage of the former. Our approach is based on the fundamental observation that presheaf categories of sorted sets are suitable universes to model call-by-(push)-value languages, and that natural, coalgebraic notions of program equivalence such as applicative similarity and logical relations can be developed within. Starting from this observation, we formalize fine-grain call-by-value and call-by-push-value in the higher-order abstract GSOS framework, reduce their key congruence properties to simple syntactic conditions by leveraging existing theory and argue that introducing changes to either language incurs minimal proof overhead.
2024
LICS
Bialgebraic Reasoning on Higher-Order Program Equivalence
Sergey Goncharov, Stefan Milius, Stelios Tsampas, and Henning Urbat
In 39th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS 2024), Jan 2024
