@inproceedings{10.1007/978-3-319-08918-8_12,
    Abstract = {We give a coinductive proof of confluence, up to equivalence of root-active subterms, of infinitary lambda-calculus. We also show confluence of B{\"o}hm reduction (with respect to root-active terms) in infinitary lambda-calculus. In contrast to previous proofs, our proof makes heavy use of coinduction and does not employ the notion of descendants.},
    Address = {Cham},
    Author = {Czajka, {\L}ukasz},
    BookTitle = {Rewriting and Typed Lambda Calculi},
    Editor = {Dowek, Gilles},
    File = {A Coinductive Confluence Proof for Infinitary Lambda-Calculus - coind (0) - a - a - u.pdf},
    ISBN = {978-3-319-08918-8},
    Pages = {164--178},
    Publisher = {Springer International Publishing},
    Title = {A Coinductive Confluence Proof for Infinitary Lambda-Calculus},
    Year = {2014},
    date-added = {2019-09-21 12:03:25 +0200},
    date-modified = {2019-09-21 12:03:25 +0200},
    doi = {10.1007/978-3-319-08918-8_12}
}

@inproceedings{10.1007/978-3-319-08918-8_12, Abstract = {We give a coinductive proof of confluence, up to equivalence of root-active subterms, of infinitary lambda-calculus. We also show confluence of B{\"o}hm reduction (with respect to root-active terms) in infinitary lambda-calculus. In contrast to previous proofs, our proof makes heavy use of coinduction and does not employ the notion of descendants.}, Address = {Cham}, Author = {Czajka, {\L}ukasz}, BookTitle = {Rewriting and Typed Lambda Calculi}, Editor = {Dowek, Gilles}, File = {A Coinductive Confluence Proof for Infinitary Lambda-Calculus - coind (0) - a - a - u.pdf}, ISBN = {978-3-319-08918-8}, Pages = {164--178}, Publisher = {Springer International Publishing}, Title = {A Coinductive Confluence Proof for Infinitary Lambda-Calculus}, Year = {2014}, date-added = {2019-09-21 12:03:25 +0200}, date-modified = {2019-09-21 12:03:25 +0200}, doi = {10.1007/978-3-319-08918-8_12} }