#### 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.
dvi

ML code:
alphabetic /
de Bruijn

BibTeX:

@inproceedings{Nipkow-LICS-93,
author="Tobias Nipkow",
title="Functional Unification of Higher-Order Patterns",
booktitle="Proc.\ 8th IEEE Symp.\ Logic in Computer Science",
pages="64--74",year=1993}