Ł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 calculus

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: March 11, 2020
    Submitted on: August 17, 2018
    Keywords: Computer Science - Logic in Computer Science
    Fundings :
      Source : OpenAIRE Research Graph
    • Infinitary Rewriting for Type Systems; Funder: European Commission; Code: 704111

    Linked data

    Source : ScholeXplorer HasVersion DOI 10.48550/arxiv.1808.05481
    • 10.48550/arxiv.1808.05481
    A new coinductive confluence proof for infinitary lambda calculus
    Czajka, Łukasz ;

    Share

    Consultation statistics

    This page has been seen 376 times.
    This article's PDF has been downloaded 396 times.