AI 中文总结
该研究在Beluga证明助手里形式化π演算的强带刺相似性，通过扩展先前工作纳入复制，基于刺和内部动作给出行为等价的共归纳编码，利用Beluga的共归纳得到简洁证明，证明了结合相关方法机械化并发演算的有效性。
AI 中文摘要
我们在Beluga证明助手里将π演算的强带刺相似性形式化，完成了一系列针对并发演算形式化基准的工作。通过扩展先前的发展以纳入复制，我们基于刺和内部动作给出了行为等价的共归纳编码。利用Beluga基于余模式的共归纳，我们得到简洁且可组合的证明，包括兼容性属性和刻画带刺预同余的上下文引理。该案例研究证明了结合高阶抽象语法和共归纳推理来机械化并发演算的有效性。
英文摘要
We formalize strong barbed similarity for the pi-calculus in the Beluga proof assistant, completing a line of work addressing the Concurrent Calculi Formalization Benchmark. By extending previous developments to include replication, we give a coinductive encoding of behavioral equivalence based on barbs and internal actions. Using Beluga's copattern-based coinduction, we obtain concise and compositional proofs, including compatibility properties and a context lemma characterizing barbed precongruence. The case study demonstrates the effectiveness of combining HOAS and coinductive reasoning for mechanizing concurrent calculi.
CommentsIn Proceedings LFMTP 2026, arXiv:2607.10318
Journal refEPTCS 448, 2026, pp. 1-17
