Unification via Explicit Substitutions: The Case of Higher-Order Patterns

Following the general method and related completeness results on using explicitsubstitutions to perform higher-order unification proposed in [5], we investigate inthis paper the case of higher-order patterns as introduced by Miller. We show thatour general algorithm specializes in a very convenient way to patterns. We alsosketch an efficient implementation of the abstract algorithm and its generalizationto constraint simplification.1 IntroductionTyped -calculi of various sorts are used...