一句话：提出一套系统化方法，用于证明带 η-展开的外延正规形式互模拟及其 up-to context 技术的可靠性。
正规形式互模拟是一种简单易用的行为等价，它通过把 λ-演算项的规范形式分解为互模拟的子项来建立项之间的关系，并且通常支持 bisimulation up to context 等强力的 up-to 技术，从而进一步简化互模拟证明。然而，在存在 η-展开的情况下，证明这类关系的可靠性变得复杂，通常依赖随语言而异的 ad hoc 证明方法。本文提出一种更系统的证明方法，用以说明外延正规形式互模拟及其相应的 up to context 技术是可靠的。作者用三种演算来展示该方法：按值调用 λ-演算、带定界控制操作符 shift 与 reset 的按值调用 λ-演算，以及带终止式控制操作符 call/cc 与 abort 的按值调用 λ-演算。前两种情形此前不存在能验证 η-律的可靠 up to context 技术，而带 call/cc 与 abort 的演算则尚无正规形式互模拟理论。所有结果均已在 Coq 证明助手中完整形式化。
Normal-form bisimilarity is a simple, easy-to-use behavioral equivalence that relates terms in $\lambda$-calculi by decomposing their normal forms into bisimilar subterms. Moreover, it typically allows for powerful up-to techniques, such as bisimulation up to context, which simplify bisimulation proofs even further. However, proving soundness of these relations becomes complicated in the presence of $\eta$-expansion and usually relies on ad hoc proof methods which depend on the language. In this paper we propose a more systematic proof method to show that an extensional normal-form bisimilarity along with its corresponding up to context technique are sound. We illustrate our technique with three calculi: the call-by-value $\lambda$-calculus, the call-by-value $\lambda$-calculus with the delimited-control operators shift and reset, and the call-by-value $\lambda$-calculus with the abortive control operators call/cc and abort. In the first two cases, there was previously no sound up to context technique validating the $\eta$-law, whereas no theory of normal-form bisimulations for a calculus with call/cc and abort has been presented before. Our results have been fully formalized in the Coq proof assistant.
@article{paperbot806,
title = {Proving Soundness of Extensional Normal-Form Bisimilarities},
author = {Dariusz Biernacki and Serguei Lenglet and Piotr Polesiuk},
journal = {Logical Methods in Computer Science},
volume = {Volume 15, Issue 1},
year = {2019},
doi = {10.23638/lmcs-15(1:31)2019}
}