通过一阶转移系统实现高阶语言的模块化余归纳 up-to 技术
Modular coinduction up-to for higher-order languages via first-order transition systems
AI总结：
本文通过完全抽象翻译将一阶LTS上的up-to双模拟技术推广到高阶语言（π-演算、λ-演算及带引用的λ-演算），仅需手动验证新语言特有技术的相容性。
摘要：
双模拟证明方法可以通过采用“up-to 双模拟”技术来增强。针对一阶（即类 CCS）带标签的转移系统（LTS）和双模拟，已经基于抽象不动点理论和相容函数发展了一套全面的此类增强理论。我们将该理论迁移到双模拟和 LTS 超越一阶模型的语言上。该方法的核心在于将更复杂的 LTS 和双模拟完全抽象地翻译到一阶系统上。这使得我们能够直接重用一阶 LTS 上可用的大量 up-to 技术库。唯一需要手动提供的要素是针对新语言特有的基本 up-to 技术的相容性。我们在 π-演算、λ-演算以及带引用的（按值调用）λ-演算上研究了该方法。
英文摘要：
The bisimulation proof method can be enhanced by employing `bisimulations up-to' techniques. A comprehensive theory of such enhancements has been developed for first-order (i.e., CCS-like) labelled transition systems (LTSs) and bisimilarity, based on abstract fixed-point theory and compatible functions. We transport this theory onto languages whose bisimilarity and LTS go beyond those of first-order models. The approach consists in exhibiting fully abstract translations of the more sophisticated LTSs and bisimilarities onto the first-order ones. This allows us to reuse directly the large corpus of up-to techniques that are available on first-order LTSs. The only ingredient that has to be manually supplied is the compatibility of basic up-to techniques that are specific to the new languages. We investigate the method on the pi-calculus, the lambda-calculus, and a (call-by-value) lambda-calculus with references.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
