More Church-Rosser Proofs in BELUGA
<|reference_start|>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 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.<|reference_end|>
@article{momigliano2024more,
    title={More Church-Rosser Proofs in BELUGA},
    author={Alberto Momigliano (Dipartimento di Informatica, Universit`a degli
  Studi di Milano, Italy), Martina Sassella (Dipartimento di Matematica,
  Universit`a degli Studi di Milano, Italy)},
    journal={EPTCS 402, 2024, pp. 34-42},
    year={2024},
    doi={10.4204/EPTCS.402.6},
    archivePrefix={arXiv},
    eprint={2404.14921},
    primaryClass={cs.LO cs.PL}
}