More Church-Rosser Proofs in BELUGA
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...
| Published in: | Electronic Proceedings in Theoretical Computer Science |
|---|---|
| Main Author: | |
| Other Authors: | |
| Format: | Article in Journal/Newspaper |
| Language: | English |
| Published: |
2024
|
| Subjects: | |
| Online Access: | https://hdl.handle.net/2434/1047908 https://doi.org/10.4204/EPTCS.402.6 https://arxiv.org/abs/2404.14921v1 |
| Summary: | 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. |
|---|