تقرير
More Church-Rosser Proofs in BELUGA
| العنوان: | More Church-Rosser Proofs in BELUGA |
|---|---|
| المؤلفون: | Momigliano, Alberto, Sassella, Martina |
| المصدر: | EPTCS 402, 2024, pp. 34-42 |
| سنة النشر: | 2024 |
| المجموعة: | Computer Science |
| مصطلحات موضوعية: | Computer Science - Logic in Computer Science, Computer Science - Programming Languages |
| الوصف: | 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. Comment: In Proceedings LSFA/HCVS 2023, arXiv:2404.13672 |
| نوع الوثيقة: | Working Paper |
| DOI: | 10.4204/EPTCS.402.6 |
| URL الوصول: | http://arxiv.org/abs/2404.14921 |
| رقم الأكسشن: | edsarx.2404.14921 |
| قاعدة البيانات: | arXiv |
| DOI: | 10.4204/EPTCS.402.6 |
|---|