Higher-order unification via explicit substitutions
Gilles Dowek, Thérèse Hardin, Claude Kirchner · 2002
Higher-order unification is equational unification for /spl beta//spl eta/-conversion, but it is not first-order equational unification, as substitution has to avoid capture. In this paper higher-order unification is reduced to first-order equational unification in a suitable theory: the /spl lambda//spl sigma/-calculus of explicit substitutions.