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 has been successfully applied to obtain 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 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 the SKI calculus and the $λ$-calculus w.r.t. a strong variant of Abramsky's applicative bisimilarity are obtained as instances.

翻译：高阶语言中的组合性证明以繁琐著称，而保证组合性的通用语义框架则难以获得。特别是，Turi 和 Plotkin 的双代数抽象 GSOS 框架已成功应用于为一阶语言获取现成的组合性结果，但迄今尚未适用于高阶语言。在本工作中，我们发展了面向高阶语言的抽象 GSOS 规范理论，实质上将 Turi 和 Plotkin 框架的核心原则迁移到了高阶设置中。在我们的理论中，高阶语言的操作语义由某些双自然变换表示，我们将其称为带点的高阶 GSOS 律。我们给出了一项适用于所有以此方式规范的系统的一般性组合性结果，并讨论了 SKI 演算和 λ 演算相对于 Abramsky 应用双相似的强变体如何作为实例获得组合性。