TY - GEN
T1 - Functional unification of higher-order patterns
AU - Nipkow, Tobias
PY - 1993
Y1 - 1993
N2 - 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, the result a directly executable functional program. In a final development step the result is adapted to λ-terms in de Bruijn's notation. The algorithms work for both simply typed and untyped terms.
AB - 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, the result a directly executable functional program. In a final development step the result is adapted to λ-terms in de Bruijn's notation. The algorithms work for both simply typed and untyped terms.
UR - http://www.scopus.com/inward/record.url?scp=0027208449&partnerID=8YFLogxK
U2 - 10.1109/lics.1993.287599
DO - 10.1109/lics.1993.287599
M3 - Conference contribution
AN - SCOPUS:0027208449
SN - 0818631422
SN - 9780818631429
T3 - Proceedings - Symposium on Logic in Computer Science
SP - 64
EP - 72
BT - Logic in Computer Science
PB - Publ by IEEE
T2 - Proceedings of the Eighth Annual IEEE Symposium on Logic in Computer Science
Y2 - 19 June 1993 through 23 June 1993
ER -