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.

翻译：Turi与Plotkin提出的双代数抽象GSOS框架为编程语言与进程语言的操作语义与指称语义建模提供了优雅的范畴论方法。在抽象GSOS中，互模拟恒为同余关系，且与指称等价性完全一致。这使语言设计者无需通过复杂特设的推理即可确立这些性质。近期，抽象GSOS风格的操作语义之双代数视角已扩展至高阶语言，同时保持了互模拟的组合性。然而，根据Turi与Plotkin原始构想，在高阶语境下对双代数指称语义的范畴论理解迄今仍属空白。本文发展了高阶抽象GSOS中的充分指称语义理论。指称模型以适当选取的语义域为参数，该语义域表现为行为双函子的局部终余代数，其构造与语言语法完全解耦。我们的方法涵盖了现有的指称语义描述，例如通过通用步进索引构建的语义域（此前需针对每种语言单独引入），并证明可适用于广泛的高阶语言，如简单类型与无类型语言，或具有概率性、非确定性分支等计算效应的语言。