论文标题
通过一阶过渡系统适用于高阶语言的模块化共同诱导
Modular coinduction up-to for higher-order languages via first-order transition systems
论文作者
论文摘要
可以通过采用“两次仿真”技术来增强双仿真方法。基于抽象的固定点理论和兼容函数，已经针对标记过渡系统（LTSS）和双相似性的一阶（类似CCS）的一阶（即CCS样）制定了这种增强的综合理论。 我们将这种理论传输到语言上，其双含量和LTS远远超出了一阶模型的语言。该方法包括将更复杂的LTS和双相似性的完全抽象的翻译到一阶上。这使我们可以直接重复使用一阶LTSS上可用的最新技术的大型语料库。必须手动提供的唯一要素是针对新语言的基本技术的兼容性。我们研究了带有参考文献的Pi-Calculus，Lambda-Calculus和（逐个呼叫）Lambda-Calculus的方法。
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.
