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的适用互模拟的强变体的组合性作为实例导出。