一句话：在高阶 abstract GSOS 框架下给出参数化、与语法解耦的双代数指称语义理论。
Turi 与 Plotkin 的双代数 abstract GSOS 框架以范畴论方式统一操作语义与指称语义，其中双相似性自动成为同余并与指称等价一致；该视角近来已推广到高阶语言，但高阶情形下一直缺乏对双代数指称语义的范畴论刻画。本文提出高阶 abstract GSOS 下的 adequate 指称语义理论：指称模型以行为双函子的局部终余代数（locally final coalgebra）作为语义域参数，其构造与语言语法完全解耦，因而语言设计者只需选定合适的语义域即可获得指称模型。该框架统一并推广了以往按语言逐一引入的一般 step-indexing 语义域，并可应用于范围广泛的高阶语言，例如简单类型与无类型语言，以及带概率或非确定性分支等计算效应的语言。
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.
DOI 原文 · arXiv · PDF（开放获取） · DBLP
@article{abs-2602-18295,
title = {Towards a Higher-Order Bialgebraic Denotational Semantics},
author = {Sergey Goncharov and Marco Peressotti and Stelios Tsampas and Henning Urbat and Stefano Volpe},
journal = {Proceedings of the ACM on Programming Languages},
volume = {10},
number = {ICFP},
year = {2026},
doi = {10.1145/3828693}
}