A generic algorithm for pre-unification modulo beta-eta-conversion and an arbitrary subtype relation is presented. Furthermore it is shown that unification w.r.t. any subtype relation is universal.
BibTeX:
@inproceedings{Nipkow-Qian-CADE-92,
author="Tobias Nipkow and Zhenyu Qian",
title="Reduction and Unification in Lambda Calculi with Subtypes",
booktitle="Proc.\ 11th Int.\ Conf.\ Automated Deduction",year=1992,
editor="Deepak Kapur",
publisher=Springer,series=LNCS,volume=607,pages="66--78"}
A revised version appeared in
Journal of Automated Reasoning.