A new coinductive confluence proof for infinitary lambda calculus
Logic in Computer Science
2023-06-22 v4
Abstract
We present a new and formal coinductive proof of confluence and normalisation of B\"ohm reduction in infinitary lambda calculus. The proof is simpler than previous proofs of this result. The technique of the proof is new, i.e., it is not merely a coinductive reformulation of any earlier proofs. We formalised the proof in the Coq proof assistant.
Keywords
Cite
@article{arxiv.1808.05481,
title = {A new coinductive confluence proof for infinitary lambda calculus},
author = {Łukasz Czajka},
journal= {arXiv preprint arXiv:1808.05481},
year = {2023}
}
Comments
arXiv admin note: text overlap with arXiv:1501.04354