一句话：提出范畴框架，抽象证明应用型互模拟自动同余，统一Howe格式下高阶语言。
应用型互模拟是call-by-name λ演算中观察等价的一种余归纳刻画，Howe曾证明其为同余，并推广到符合特定格式的语言。本文提出一个范畴框架，用于指定操作语义，并在该抽象层面证明应用型互模拟的类似物自动具有同余性。该框架覆盖call-by-name、call-by-value以及非确定性λ演算中的标准应用型互模拟，并涵盖符合Howe格式变体的所有语言，从而给出统一且可复用的同余性证明方法。
Applicative bisimilarity is a coinductive characterisation of observational equivalence in call-by-name lambda-calculus, introduced by Abramsky (1990). Howe (1996) gave a direct proof that it is a congruence, and generalised the result to all languages complying with a suitable format. We propose a categorical framework for specifying operational semantics, in which we prove that (an abstract analogue of) applicative bisimilarity is automatically a congruence. Example instances include standard applicative bisimilarity in call-by-name, call-by-value, and call-by-name non-deterministic $\lambda$-calculus, and more generally all languages complying with a variant of Howe's format.
@article{paperbot1651,
title = {A categorical framework for congruence of applicative bisimilarity in higher-order languages},
author = {Tom Hirschowitz and Ambroise Lafont},
journal = {Logical Methods in Computer Science},
volume = {Volume 18, Issue 3},
year = {2022},
doi = {10.46298/lmcs-18(3:37)2022}
}