Higher Order Unification via Explicit Substitutions
            Fairouz Kamareddine, Heriot-Watt University
    Joint Work with Mauricio Ayala-Rincon, University of Brasilia


In the area of Explicit substitutions with open terms (holes), there
are two styles: the lambda sigma style [1] where there are two sorts
of objects (terms and substitutions), and the lambda se [5] style which
uses only one sort of objects (terms) and hence remains close to the
syntax of the lambda calculus.

Dowek, Hardin and Kirchner developed in [4] a novel higher order
unification (HOU) method based on the lambda sigma style of explicit
substitutions.  That method resolves HOU by first order unification
(FOU).  This is achieved via a pre-cooking translation of the HOU
problem into an FOU problem of the lambda sigma calculus. Solutions to
the FOU problem are then translated back into the range of the
pre-cooking translation and subsequently to solutions of the original
problem in the lambda calculus.

In [2], we studied unification in the lambda se style of explicit
substitutions and showed that lambda se unification enables quicker
detection of redices. In [3] we gave a pre-cooking translation for
applying lambda se unification to HOU in the lambda calculus. We
established correctness and completeness and showed that avoiding the
use of substitution objects makes lambda se HOU more efficient than
lambda sigma HOU.

In this talk, we present both styles of Explicit substitutions (see
also [6]) and survey both styles of HOU.  We then outline the
differences between these HOU-styles.

[1] M. Abadi, L. Cardelli, P-L. Curien and J-J. Levy, Explicit
Substitutions, Journal of Functional Programming 1(4):375-416, 1991.

[2] M.  Ayala-Rincon and F. Kamareddine, Unification via the lambda se
style of explicit substitutions, Logic Journal of the Interest Group
in Pure and Applied Logic (IGPL), 9(4):521-555, 2001.

[3] M.  Ayala-Rincon and F. Kamareddine, On Applying the lambda
se-style of unification for simply-typed higher order unification in
the pure lambda calculus, Submitted.

[4] G. Dowek, T. Hardin and C. Kirchner, Higher-Order unification via
explicit substitutions, Information and Computation, 157(1/2):183-235,
2000.

[5] F. Kamareddine and A. Rios, Extending a lambda calculus with
explicit substitution which preserves Strong Normalisation into a
confluent calculus on open terms, Journal of Functional Programming
7(4):395-420, 1997.

[6] F. Kamareddine and A. Rios, Relating the Lambda-sigma and Lambda-s
styles of Explicit Substitutions, Journal of Logic and Computation 10
(3):349-380, 2000.