Functional Unification of Higher-Order Patterns

Tobias Nipkow

The complete development of a unification algorithm for so-called higher-order patterns, a subclass of lambda-terms, is presented. The starting point is a formulation of unification by transformation, the result a directly executable functional program. In a final development step the result is adapted to lambda-terms in de Bruijn's notation. The algorithms work for both simply typed and untyped terms.


ML code: alphabetic / de Bruijn


author="Tobias Nipkow",
title="Functional Unification of Higher-Order Patterns",
booktitle="Proc.\ 8th IEEE Symp.\ Logic in Computer Science",