Using First-Order Narrowing To Solve Goals Of Higher-Order Patterns
In this paper we propose a modular algorithm
for higher-order pattern unification
modulo a first-order term rewrite system.
The modular algorithm is parameterized by a first-order narrowing algorithm
and thus may lay a foundation for combining first-order functional logic
programming and higher-order logic programming based on higher-order patterns.
The abstract formulation of the modular algorithm clearly shows
where else it can be applied.
The paper is here.