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}