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...

Full description

Bibliographic Details
Published in:Electronic Proceedings in Theoretical Computer Science
Main Authors: A. Momigliano, M. Sassella
Format: Article in Journal/Newspaper
Language:English
Published: Open Publishing Association 2024
Subjects:
Settore INF/01 - Informatica
Eta
Lambda
Beluga
Beluga*
Online Access:https://hdl.handle.net/2434/1047908
https://doi.org/10.4204/EPTCS.402.6
https://arxiv.org/abs/2404.14921v1
id ftunivmilanoair:oai:air.unimi.it:2434/1047908
record_format openpolar
spelling ftunivmilanoair:oai:air.unimi.it:2434/1047908 2024-09-09T19:33:16+00:00 More Church-Rosser Proofs in BELUGA A. Momigliano M. Sassella A. Momigliano M. Sassella 2024 https://hdl.handle.net/2434/1047908 https://doi.org/10.4204/EPTCS.402.6 https://arxiv.org/abs/2404.14921v1 eng eng Open Publishing Association International Workshop on Logical and Semantic Frameworks, with Applications (LSFA) and 10th Workshop on Horn Clauses for Verification and Synthesis (HCVS) : 1 through 2 July volume:402 firstpage:34 lastpage:42 numberofpages:9 journal:ELECTRONIC PROCEEDINGS IN THEORETICAL COMPUTER SCIENCE https://hdl.handle.net/2434/1047908 doi:10.4204/EPTCS.402.6 info:eu-repo/semantics/altIdentifier/scopus/2-s2.0-85191663053 https://arxiv.org/abs/2404.14921v1 info:eu-repo/semantics/openAccess Settore INF/01 - Informatica info:eu-repo/semantics/article 2024 ftunivmilanoair https://doi.org/10.4204/EPTCS.402.6 2024-08-26T23:45:11Z 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. Article in Journal/Newspaper Beluga Beluga* The University of Milan: Archivio Istituzionale della Ricerca (AIR) Eta ENVELOPE(-62.917,-62.917,-64.300,-64.300) Lambda ENVELOPE(-62.983,-62.983,-64.300,-64.300) Electronic Proceedings in Theoretical Computer Science 402 34 42
institution Open Polar
collection The University of Milan: Archivio Istituzionale della Ricerca (AIR)
op_collection_id ftunivmilanoair
language English
topic Settore INF/01 - Informatica
spellingShingle Settore INF/01 - Informatica
A. Momigliano
M. Sassella
More Church-Rosser Proofs in BELUGA
topic_facet Settore INF/01 - Informatica
description 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.
author2 A. Momigliano
M. Sassella
format Article in Journal/Newspaper
author A. Momigliano
M. Sassella
author_facet A. Momigliano
M. Sassella
author_sort A. Momigliano
title More Church-Rosser Proofs in BELUGA
title_short More Church-Rosser Proofs in BELUGA
title_full More Church-Rosser Proofs in BELUGA
title_fullStr More Church-Rosser Proofs in BELUGA
title_full_unstemmed More Church-Rosser Proofs in BELUGA
title_sort more church-rosser proofs in beluga
publisher Open Publishing Association
publishDate 2024
url https://hdl.handle.net/2434/1047908
https://doi.org/10.4204/EPTCS.402.6
https://arxiv.org/abs/2404.14921v1
long_lat ENVELOPE(-62.917,-62.917,-64.300,-64.300)
ENVELOPE(-62.983,-62.983,-64.300,-64.300)
geographic Eta
Lambda
geographic_facet Eta
Lambda
genre Beluga
Beluga*
genre_facet Beluga
Beluga*
op_relation International Workshop on Logical and Semantic Frameworks, with Applications (LSFA) and 10th Workshop on Horn Clauses for Verification and Synthesis (HCVS) : 1 through 2 July
volume:402
firstpage:34
lastpage:42
numberofpages:9
journal:ELECTRONIC PROCEEDINGS IN THEORETICAL COMPUTER SCIENCE
https://hdl.handle.net/2434/1047908
doi:10.4204/EPTCS.402.6
info:eu-repo/semantics/altIdentifier/scopus/2-s2.0-85191663053
https://arxiv.org/abs/2404.14921v1
op_rights info:eu-repo/semantics/openAccess
op_doi https://doi.org/10.4204/EPTCS.402.6
container_title Electronic Proceedings in Theoretical Computer Science
container_volume 402
container_start_page 34
op_container_end_page 42
_version_ 1809902667817811968

Similar Items