Higher-order abstract GSOS is a recent extension of Turi and Plotkin's framework of Mathematical Operational Semantics to higher-order languages. The fundamental well-behavedness property of all specifications within the framework is that coalgebraic strong (bi)similarity on their operational model is a congruence. In the present work, we establish a corresponding congruence theorem for weak similarity, which is shown to instantiate to well-known concepts such as Abramsky's applicative similarity for the lambda-calculus. On the way, we develop several techniques of independent interest at the level of abstract categories, including relation liftings of mixed-variance bifunctors and higher-order GSOS laws, as well as Howe's method.

翻译：高阶抽象GSOS是Turi和Plotkin的数学操作语义框架在高阶语言中的近期扩展。该框架内所有规范的基本良定性性质是：操作模型上的余代数强（双）相似性构成一个同余关系。在本工作中，我们为弱相似性建立了相应的同余定理，并证明该定理可实例化为λ演算中Abramsky的应用相似性等已知概念。在此过程中，我们发展了若干具有独立意义的抽象范畴层面的技术，包括混合方差双函子的关系提升、高阶GSOS法则以及Howe方法。