Czajka, Łukasz - 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)2020
A new coinductive confluence proof for infinitary lambda calculus

Authors: Czajka, Łukasz

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.


Volume: Volume 16, Issue 1
Published on: March 11, 2020
Submitted on: August 17, 2018
Keywords: Computer Science - Logic in Computer Science


Share

Consultation statistics

This page has been seen 188 times.
This article's PDF has been downloaded 168 times.