Paper: Functional unification of higher-order patterns (at LICS 1993)

Authors: Tobias Nipkow

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

BibTeX

  @InProceedings{Nipkow-Functionalunificati,
    author = 	 {Tobias Nipkow},
    title = 	 {Functional unification of higher-order patterns},
    booktitle =  {Proceedings of the Eighth Annual IEEE Symposium on Logic in Computer Science (LICS 1993)},
    year =	 {1993},
    month =	 {June}, 
    pages =      {64--74},
    location =   {Montreal, Canada}, 
    publisher =	 {IEEE Computer Society Press}
  }