@INPROCEEDINGS{salvati03a,
AUTHOR = {Sylvain Salvati and Philippe de Groote},
TITLE = {On the complexity of higher-order matching in the linear $\lambda$-calculus},
BOOKTITLE = {{International Conference on Rewriting Techniques and Applications - RTA'2003, Valencia, Spain}},
YEAR ={2003},
EDITOR = {Robert Nieuwenhuis},
VOLUME = {2706},
SERIES = {Lecture notes in Computer Science},
PAGES = {234-245},
MONTH ={Jun},
KEYWORDS = {lambda-calculus, linear logic, unification, matching},
ABSTRACT = {We prove that linear second-order matching in the linear $\lambda$-calculus with linear occurrences of the unknowns is NP-complete. This result shows that context matching and second-order matching in the linear $\lambda$-calculus are, in fact, two different problems.},
}