Title :
Functional unification of higher-order patterns
Author_Institution :
Inst. fuer Inf., Munchen Univ., Germany
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;
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
DOI :
10.1109/LICS.1993.287599
