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 (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.

翻译：高阶语言的组合性证明以其复杂性著称，而能够保证组合性的通用语义框架更是难以构建。特别是Turi与Plotkin提出的双代数抽象GSOS框架（可为初阶语言提供现成的组合性结果），至今尚未能应用于高阶语言。本工作发展了一套面向高阶语言的抽象GSOS规范理论，实质性地将Turi与Plotkin框架的核心原理迁移至高阶场景。在该理论中，高阶语言的操作语义通过我们称为（带指针的）高阶GSOS律的某种余自然变换来刻画。我们给出适用于所有以此方式规范的系统的一般组合性结果，并论述如何将组合逻辑与λ-演算关于Abramsky强应用互模拟的相应组合性作为实例导出。