@conference {IIIA-1996-1256,
title = {Linear Second Order Unification},
booktitle = {Lecture Notes in Computer Science},
volume = {1103},
year = {1996},
pages = {332-346},
publisher = {Springer-Verlag},
organization = {Springer-Verlag},
abstract = {We present a new class of second-order unification problems, which we have called linear. We deal with completely general second-order typed unification problems, but we restrict the set of unifiers under consideration: they instantiate free variables by linear terms, i.e. terms where any lambda-abstractions bind one and only one occurrence of a bound variable. Linear second-order unification properly extends context unification studied by Comon and Schmidt-Schauss. We describe a sound and complete procedure for this class of unification problems and we prove termination for three different subcases of them. One of these subcases is obtained requiring Comon{\textquoteright}s condition, another corresponds to Schmidt-Schauss{\textquoteright}s condition, (both studied previously for the case of context unification, and applied here to a larger class of problems), and the third one is original, namely that free variables occur at most twice.},
author = {Jordi Levy}
}