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应用互模拟的强化变种的组合性作为实例获得。