@article {IOPORT.01915463,
    author       = {Dezani-Ciancaglini, Mariangiola and Severi, Paula and de Vries, Fer-Jan},
    title        = {Infinitary lambda calculus and discrimination of Berarducci trees.},
    year         = {2003},
    journal      = {Theoretical Computer Science},
    volume       = {298},
    number       = {2},
    issn         = {0304-3975},
    pages        = {275-302},
    publisher    = {Elsevier Science Publishers, Amsterdam},
    doi          = {10.1016/S0304-3975(02)00809-5},
    abstract     = {Summary: We propose an extension of lambda calculus for which the Berarducci trees equality coincides with observational equivalence, when we observe rootstable or rootactive behavior of terms. In one direction the proof is an adaptation of the classical B\"ohm out technique. In the other direction the proof is based on confluence for strongly converging reductions in this extension.},
    identifier   = {01915463},
}