Towards a Higher-Order Bialgebraic Denotational Semantics

TL;DR

This paper develops a higher-order bialgebraic denotational semantics framework that generalizes existing models, ensuring compositionality and applicability to various higher-order languages with effects.

Contribution

It introduces a categorical theory of denotational semantics for higher-order languages within the abstract GSOS framework, decoupling semantics from syntax.

Findings

Captures existing semantic models like step-indexing

Applicable to a wide range of higher-order languages

Ensures compositionality of bisimilarity in higher-order settings

Abstract

The bialgebraic abstract GSOS framework by Turi and Plotkin provides an elegant categorical approach to modelling the operational and denotational semantics of programming and process languages. In abstract GSOS, bisimilarity is always a congruence, and it coincides with denotational equivalence. This saves the language designer from intricate, ad-hoc reasoning to establish these properties. The bialgebraic perspective on operational semantics in the style of abstract GSOS has recently been extended to higher-order languages, preserving compositionality of bisimilarity. However, a categorical understanding of bialgebraic denotational semantics according to Turi and Plotkin's original vision has so far been missing in the higher-order setting. In the present paper, we develop a theory of adequate denotational semantics in higher-order abstract GSOS. The denotational models are parametric in an appropriately chosen semantic domain in the form of a locally final coalgebra for a behaviour bifunctor, whose construction is fully decoupled from the syntax of the language. Our approach captures existing accounts of denotational semantics such as semantic domains built via general step-indexing, previously introduced on a per-language basis, and is shown to be applicable to a wide range of different higher-order languages, e.g. simply typed and untyped languages, or languages with computational effects such as probabilistic or non-deterministic branching.