Linear higher-order pre-unification

We develop an efficient representation and a pre-unification algorithm in the style of Huet for the linear lambda-calculus lambda(-->-O&T) which includes intuitionistic functions (-->), linear functions (-o), additive pairing (&), and additive unit (T). Applications lie in proof search, logic programming, and logical frameworks based on linear type theories. We also show that, surprisingly, a similar pre-unification algorithm does not exist for certain sublanguages.