一句话：提出高阶抽象GSOS理论，以dinatural变换刻画高阶语言操作语义，并给出通用组合性结果。
高阶语言的操作语义组合性证明通常十分复杂，且缺乏保证组合性的通用语义框架。Turi与Plotkin的双代数抽象GSOS框架为一阶语言提供了现成的组合性结果，但一直不适用于高阶语言。本文将抽象GSOS规范理论推广到高阶情形：用称为pointed higher-order GSOS law的dinatural变换来刻画高阶语言的操作语义，并据此给出一个适用于所有此类规范系统的通用组合性定理。作为实例，作者展示了SKI演算与λ演算相对于Abramsky应用型双模拟的强变体的组合性均可由该框架推出。
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.
@article{paperbot2083,
title = {Towards a Higher-Order Mathematical Operational Semantics},
author = {Sergey Goncharov and Stefan Milius and Lutz Schröder and Stelios Tsampas and Henning Urbat},
journal = {Proceedings of the ACM on Programming Languages},
volume = {7},
number = {POPL},
year = {2023},
doi = {10.1145/3571215}
}