高阶语言中的组合性证明极为复杂，且难以找到能够保证组合性的通用语义框架。特别是，Turi 和 Plotkin 的双代数抽象 GSOS 框架虽然为一阶语言提供了现成的组合性结果，但迄今为止尚未适用于高阶语言。在本文中，我们发展了一种针对高阶语言的抽象 GSOS 规范理论，实际上将 Turi 和 Plotkin 框架的核心原理推广到了高阶设置中。在我们的理论中，高阶语言的操作语义由某些特定的 dinatural 变换表示，我们称其为“（指针）高阶 GSOS 法则”。我们给出了一般的组合性结果，适用于所有以此方式定义的系统，并讨论了如何将组合逻辑和 λ-演算相对于 Abramsky 强形式的可应用性相似性的组合性作为特例获得。

Compositionality proofs in higher-order languages are notoriously involved, and general semantic frameworks guaranteeing compositionality are hard to come by. In particular, Turi and Plotkin's bialgebraic abstract GSOS framework, which provides off-the-shelf compositionality results for first-order languages, so far does not apply to higher-order languages. In the present work, we develop a theory of abstract GSOS specifications for higher-order languages, in effect transferring the core principles of Turi and Plotkin's framework to a higher-order setting. In our theory, the operational semantics of higher-order languages is represented by certain dinatural transformations that we term \emph{(pointed) higher-order GSOS laws}. We give a general compositionality result that applies to all systems specified in this way and discuss how compositionality of combinatory logics and the $\lambda$-calculus w.r.t.\ a strong variant of Abramsky's applicative bisimilarity are obtained as instances.