link: UNIF'03 is at
UNIF is the main international meeting on unification. Unification is
concerned with the problem of identifying given terms, either syntactically
or modulo a given logical theory. Syntactic unification is the basic
operation of most automated reasoning systems, and unification modulo
theories can be used, for instance, to build in special equational
theories into theorem provers.
Workshop web page with more