Unification of higher-order patterns in linear time and space

Higher-order patterns are simply typed X-terms in long beta-normal form where the arguments of a free variable are always eta-equal to distinct bound variables. It has been proved that unification of higher-order patterns module alpha, beta and eta reductions in the simply typed lambda-calculus is decidable and unifiable higher-order patterns have a most general unifier. In this paper a unification algorithm for higher-order patterns is presented, whose time and space complexities are proved to be linear in the size of input.