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.

翻译：高阶语言的组合性证明历来复杂，而能确保组合性的通用语义框架则更为罕见。具体而言，Turi和Plotkin的双代数抽象GSOS框架虽为一阶语言提供了现成的组合性结果，但迄今未能适用于高阶语言。本文针对高阶语言发展了一套抽象GSOS规范理论，实质上是将Turi和Plotkin框架的核心原理迁移至高阶语境。在我们的理论中，高阶语言的操作语义由特定的双自然变换（我们称之为\emph{（带点）高阶GSOS律}）所刻画。我们给出了适用于所有以此方式指定系统的通用组合性定理，并探讨了如何将组合逻辑及$\lambda$-演算相对于Abramsky应用互模拟强变种的组合性作为该定理的特例予以推导。