@inproceedings{10.1007/3-540-56610-4_78,
    Abstract = {Higher-order patterns are simply typed ${\l}ambda$-terms in $\eta$-long form where free variables F only occur in the form F(x1,...,xk) with x1, ...,xkbeing distinct bound variables. It has been proved in [6] that in the simply typed ${\l}ambda$-calculus unification of higher-order patterns modulo $\alpha$, $\beta$ and $\eta$ reductions is decidable and unifiable higher-order patterns have a most general unifier.},
    Address = {Berlin, Heidelberg},
    Author = {Qian, Zhenyu},
    BookTitle = {TAPSOFT'93: Theory and Practice of Software Development},
    Editor = {Gaudel, M. -C. and Jouannaud, J. -P.},
    File = {Linear unification of higher-order patterns - Qian1993\_Chapter\_LinearUnificationOfHigher-orde - a - a - i.pdf},
    ISBN = {978-3-540-47598-9},
    Pages = {391--405},
    Publisher = {Springer Berlin Heidelberg},
    Title = {Linear unification of higher-order patterns},
    Year = {1993},
    date-added = {2019-08-08 11:15:29 +0200},
    date-modified = {2019-08-08 11:15:29 +0200},
    doi = {10.1007/3-540-56610-4_78}
}

@inproceedings{10.1007/3-540-56610-4_78, Abstract = {Higher-order patterns are simply typed ${\l}ambda$-terms in $\eta$-long form where free variables F only occur in the form F(x1,...,xk) with x1, ...,xkbeing distinct bound variables. It has been proved in [6] that in the simply typed ${\l}ambda$-calculus unification of higher-order patterns modulo $\alpha$, $\beta$ and $\eta$ reductions is decidable and unifiable higher-order patterns have a most general unifier.}, Address = {Berlin, Heidelberg}, Author = {Qian, Zhenyu}, BookTitle = {TAPSOFT'93: Theory and Practice of Software Development}, Editor = {Gaudel, M. -C. and Jouannaud, J. -P.}, File = {Linear unification of higher-order patterns - Qian1993_Chapter_LinearUnificationOfHigher-orde - a - a - i.pdf}, ISBN = {978-3-540-47598-9}, Pages = {391--405}, Publisher = {Springer Berlin Heidelberg}, Title = {Linear unification of higher-order patterns}, Year = {1993}, date-added = {2019-08-08 11:15:29 +0200}, date-modified = {2019-08-08 11:15:29 +0200}, doi = {10.1007/3-540-56610-4_78} }