Ł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)2020
A new coinductive confluence proof for infinitary lambda calculusArticle

Authors: Łukasz Czajka

    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
    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 1340 times.
    This article's PDF has been downloaded 463 times.