@article{Loader01012003,
    Abstract = {We show that the solvability of matching problems in the simply typed {$\lambda$}-calculus, up to {$\beta$} equivalence, is not decidable. This decidability question was raised by Huet [4].Note that there are two variants of the question: that concerning {$\beta$} equivalence (dealt with here), and that concerning {$\beta$}η equivalence.The second of these is perhaps more interesting; unfortunately the work below sheds no light on it, except perhaps to illustrate the subtlety and difficulty of the problem.},
    Author = {Loader, Ralph},
    EPrint = {http://jigpal.oxfordjournals.org/content/11/1/51.full.pdf+html},
    File = {Higher Order {$\beta$} Matching is Undecidable - Loader (0) (0) - a - a - a.pdf},
    Journal = {Logic Journal of IGPL},
    Keywords = {higher-order matching},
    Number = {1},
    Pages = {51-68},
    Title = {Higher Order {$\beta$} Matching is Undecidable},
    URL = {http://jigpal.oxfordjournals.org/content/11/1/51.abstract},
    Volume = {11},
    Year = {2003},
    bdsk-url-1 = {http://jigpal.oxfordjournals.org/content/11/1/51.abstract},
    bdsk-url-2 = {http://dx.doi.org/10.1093/jigpal/11.1.51},
    date-added = {2013-02-19 17:15:39 +0000},
    date-modified = {2013-02-19 17:15:54 +0000},
    file-2 = {Higher Order {$\beta$} Matching is Undecidable - Loader (1) (0) - a - a - a.pdf},
    doi = {10.1093/jigpal/11.1.51}
}

@article{Loader01012003, Abstract = {We show that the solvability of matching problems in the simply typed {$\lambda$}-calculus, up to {$\beta$} equivalence, is not decidable. This decidability question was raised by Huet [4].Note that there are two variants of the question: that concerning {$\beta$} equivalence (dealt with here), and that concerning {$\beta$}η equivalence.The second of these is perhaps more interesting; unfortunately the work below sheds no light on it, except perhaps to illustrate the subtlety and difficulty of the problem.}, Author = {Loader, Ralph}, EPrint = {http://jigpal.oxfordjournals.org/content/11/1/51.full.pdf+html}, File = {Higher Order {$\beta$} Matching is Undecidable - Loader (0) (0) - a - a - a.pdf}, Journal = {Logic Journal of IGPL}, Keywords = {higher-order matching}, Number = {1}, Pages = {51-68}, Title = {Higher Order {$\beta$} Matching is Undecidable}, URL = {http://jigpal.oxfordjournals.org/content/11/1/51.abstract}, Volume = {11}, Year = {2003}, bdsk-url-1 = {http://jigpal.oxfordjournals.org/content/11/1/51.abstract}, bdsk-url-2 = {http://dx.doi.org/10.1093/jigpal/11.1.51}, date-added = {2013-02-19 17:15:39 +0000}, date-modified = {2013-02-19 17:15:54 +0000}, file-2 = {Higher Order {$\beta$} Matching is Undecidable - Loader (1) (0) - a - a - a.pdf}, doi = {10.1093/jigpal/11.1.51} }