Peter Borovanský: Implementation of Higher-Order Unification Based on Calculus of Explicit Substitution. SOFSEM 1995: 363-368