一句话：将一阶 LTS 的 up-to 双模拟理论经全抽象翻译迁移到高阶语言，实现模块化共归纳证明。
本文研究如何把一阶标记迁移系统（LTS）上成熟的“up-to 双模拟”共归纳证明技术推广到高阶语言。已有理论基于抽象不动点与兼容函数，为 CCS 类一阶 LTS 提供了丰富的 up-to 技术库，但高阶语言的 LTS 与双相似性超出了该框架。作者提出通过构造从高阶 LTS 和双相似性到一阶 LTS 的全抽象翻译，把问题归约到一阶情形，从而直接复用现有 up-to 技术；唯一需要手工验证的是新语言特有基本 up-to 技术的兼容性。文章在 π 演算、λ 演算以及带引用的按值调用 λ 演算上实例化该方法，表明模块化 coinduction 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.
@article{paperbot1279,
title = {Modular coinduction up-to for higher-order languages via first-order transition systems},
author = {Jean-Marie Madiot and Damien Pous and Davide Sangiorgi},
journal = {Logical Methods in Computer Science},
volume = {Volume 17, Issue 3},
year = {2021},
doi = {10.46298/lmcs-17(3:25)2021}
}