Unification via λs_e-style of explicit substitution

A unification method based on the ?s_e-style of explicit substitution is proposed. This method together with appropriate translations, provide a Higher Order Unification (HOU) procedure for the pure ?-calculus. Our method is influenced by the treatment introduced by Dowek, Hardin and Kirchner using the ?s-style of explicit substitution. Correctness and completeness properties of the proposed ?s_e-unification method are shown and its advantages, inherited from the qualities of the ?s_e-calculus, are pointed out. Our method needs only one sort of objects: terms. And in contrast to the HOU approach based on the ?s-calculus, it avoids the use of substitution objects. This makes our method closer to the syntax of the ?-calculus. Furthermore, detection of redices depends on the search for solutions of simple arithmetic constraints which makes our method more operational than the one based on the ?s-style of explicit substitution.