Paper  abstract   bibtex   

@article{ a_tcs93,
  author = {Daniel J.\ Dougherty},
  title = {Higher-order unification via combinators},
  journal = {Theoretical Computer Science},
  volume = {114},
  number = {2},
  pages = {273--298},
  day = {21},
  year = {1993},
  abstract = {We present an algorithm for unification in the
                  simply typed lambda calculus which enumerates
                  complete sets of unifiers using a finitely
                  branching search space. In fact, the types of
                  terms may contain type-variables, so that a
                  solution may involve typesubstitution as well
                  as term-substitution. the problem is first
                  translated into the problem of unification with
                  respect to extensional equality in combinatory
                  logic, and the algorithm is defined in terms of
                  transformations on systems of combinatory
                  terms. These transformations are based on a new
                  method (itself based on systems) for deciding
                  extensional equality between typed combinatory
                  logic terms. },
  url = {tcs93.pdf}
}