More Church-Rosser Proofs in BELUGA
Alberto Momigliano (Dipartimento di Informatica, Universit\`a degli, Studi di Milano, Italy), Martina Sassella (Dipartimento di Matematica,, Universit\`a degli Studi di Milano, Italy)

TL;DR
This paper presents new formalizations of the Church-Rosser property in lambda-calculi using Beluga, including proofs for beta, eta, and typed calculi like System F, and explores encoding and counterexample search within Beluga.
Contribution
It introduces novel formal proofs of confluence for beta and eta reductions in lambda-calculi within Beluga, extending to typed systems and meta-logic encoding techniques.
Findings
Confluence proofs for beta-reduction in untyped lambda-calculus.
Extension of proofs to eta-reduction and System F.
Use of Beluga's logic programming for counterexample search.
Abstract
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.
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
