 |
 |
Łukasz Czajka - A new coinductive confluence proof for infinitary lambda calculus
lmcs:4757 - Logical Methods in Computer Science, March 11, 2020, Volume 16, Issue 1 - https://doi.org/10.23638/LMCS-16(1:31)2020A new coinductive confluence proof for infinitary lambda calculusArticle
We present a new and formal coinductive proof of confluence and normalisation of Böhm 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.
Source: arXiv.org:1808.05481
Volume: Volume 16, Issue 1
Published on: March 11, 2020
Accepted on: February 19, 2020
Submitted on: August 17, 2018
Keywords: Computer Science - Logic in Computer Science
Funding:
- Source : OpenAIRE Graph
- Infinitary Rewriting for Type Systems; Funder: European Commission; Code: 704111
Consultation statistics
This page has been seen 1804 times.
This article's PDF has been downloaded 545 times.