无穷λ演算的一个新的余归纳合流性证明
A new coinductive confluence proof for infinitary lambda calculus
AI总结：
本文提出了无穷λ演算中Böhm归约合流性与规范化的新余归纳证明，该证明更简单且技术新颖，并在Coq中形式化验证。
摘要：
我们给出了无穷λ演算中Böhm归约的合流性和规范化的一个新的形式化余归纳证明。该证明比之前的结果证明更简单。证明技术是新的，即它不仅仅是任何早期证明的余归纳重构。我们在Coq证明助手中形式化了该证明。
英文摘要：
We present a new and formal coinductive proof of confluence and normalisation of Böhm reduction in infinitary lambda calculus. The proof is simpler than previous proofs of this result. The technique of the proof is new, i.e., it is not merely a coinductive reformulation of any earlier proofs. We formalised the proof in the Coq proof assistant.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
