DocumentCode
1823059
Title
Functional unification of higher-order patterns
Author
Nipko, Tobias
Author_Institution
Inst. fuer Inf., Munchen Univ., Germany
fYear
1993
fDate
19-23 Jun 1993
Firstpage
64
Lastpage
74
Abstract
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
Keywords
functional programming; lambda calculus; programming theory; theorem proving; λ-terms; de Bruijn´s notation; directly executable functional program; functional unification algorithm; higher-order patterns; transformation formulation; typed terms; untyped terms; Automatic programming; Calculus; Computer languages; Geophysical measurement techniques; Ground penetrating radar; Inference algorithms; Inference mechanisms; Logic programming;
fLanguage
English
Publisher
ieee
Conference_Titel
Logic in Computer Science, 1993. LICS '93., Proceedings of Eighth Annual IEEE Symposium on
Conference_Location
Montreal, Que.
Print_ISBN
0-8186-3140-6
Type
conf
DOI
10.1109/LICS.1993.287599
Filename
287599
Link To Document