Paper: Functional unification of higher-order patterns (at LICS 1993)
Authors: Tobias NipkowAbstract
The complete development of a unification algorithm for so-called higher-order patterns, a subclass of λ-terms, is presented. The starting point is a formulation of unification by transformation, and the result a directly executable functional program. In a final development step, the result is adapted to λ-terms in de Bruijn's (1972) notation. The algorithms work for both simply typed and untyped terms
BibTeX
@InProceedings{Nipkow-Functionalunificati, author = {Tobias Nipkow}, title = {Functional unification of higher-order patterns}, booktitle = {Proceedings of the Eighth Annual IEEE Symp. on Logic in Computer Science, {LICS} 1993}, year = 1993, editor = {Moshe Vardi}, month = {June}, pages = {64--74}, location = {Montreal, Canada}, publisher = {IEEE Computer Society Press} }