We report on yet another formalization of the Church-Rosser property in lambda-calculi, carried out with the proof environment Beluga. After the well-known proofs of confluence for beta-reduction in the untyped settings, with and without Takahashi's complete developments method, we concentrate on eta-reduction and obtain the result for beta-eta modularly. We further extend the analysis to typed-calculi, in particular System F. Finally, we investigate the idea of pursuing the encoding directly in Beluga's meta-logic, as well as the use of Beluga's logic programming engine to search for counterexamples.

翻译：我们报告了在λ演算中对Church-Rosser性质的又一种形式化，该工作借助证明环境Beluga完成。在无类型设定下，我们先后给出了基于Takahashi完全展开方法及其变体的β-约化合流性的经典证明。继而聚焦于η-约化，以模块化方式获得β-η合流性结果。进一步将分析拓展至带类型λ演算，特别是System F。最后，我们探讨了直接在Beluga元逻辑中实施编码的思路，以及利用Beluga逻辑编程引擎寻找反例的可能性。