Higher-order unification via explicit substitutions Extended Abstract
Gilles Dowek, Thérèse Hardin, Claude Kirchner · 1995
Higher-order unification is equational unification for βη-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 λσ-calculus of explicit substitutions.