@article{STATMAN197973,
    Abstract = {We prove that the problem of deciding for closed terms t1, t2 of the typed {$\lambda$}-calculus whether t1 {$\beta$}-converts to t2 is not elementary recursive.},
    Author = {Statman, Richard},
    File = {1-s2.0-0304397579900070-main (0) - a - a - p.pdf},
    ISSN = {0304-3975},
    Journal = {Theoretical Computer Science},
    Keywords = {classic},
    Number = {1},
    Pages = {73 - 81},
    Title = {The typed {$\lambda$}-calculus is not elementary recursive},
    URL = {http://www.sciencedirect.com/science/article/pii/0304397579900070},
    Volume = {9},
    Year = {1979},
    bdsk-url-1 = {http://www.sciencedirect.com/science/article/pii/0304397579900070},
    bdsk-url-2 = {https://doi.org/10.1016/0304-3975(79)90007-0},
    date-added = {2019-08-07 17:51:30 +0200},
    date-modified = {2019-08-07 17:51:45 +0200},
    doi = {10.1016/0304-3975(79)90007-0}
}

@article{STATMAN197973, Abstract = {We prove that the problem of deciding for closed terms t1, t2 of the typed {$\lambda$}-calculus whether t1 {$\beta$}-converts to t2 is not elementary recursive.}, Author = {Statman, Richard}, File = {1-s2.0-0304397579900070-main (0) - a - a - p.pdf}, ISSN = {0304-3975}, Journal = {Theoretical Computer Science}, Keywords = {classic}, Number = {1}, Pages = {73 - 81}, Title = {The typed {$\lambda$}-calculus is not elementary recursive}, URL = {http://www.sciencedirect.com/science/article/pii/0304397579900070}, Volume = {9}, Year = {1979}, bdsk-url-1 = {http://www.sciencedirect.com/science/article/pii/0304397579900070}, bdsk-url-2 = {https://doi.org/10.1016/0304-3975(79)90007-0}, date-added = {2019-08-07 17:51:30 +0200}, date-modified = {2019-08-07 17:51:45 +0200}, doi = {10.1016/0304-3975(79)90007-0} }