## Reduction and Unification in Lambda Calculi with a General Notion of Subtype

### Abstract:

Reduction, equality and unification are studied for
a family of simply typed lambda calculi with subtypes. The subtype
relation is required to relate base types only to base types and to
satisfy some order-theoretic conditions. Constants are required to
have a least type, i.e. ``no overloading''. We define the usual beta-
and a subtype-dependent eta-reduction. These are related to a typed
equality relation and shown to be confluent in a certain sense. We
present a generic algorithm for pre-unification modulo
beta-eta-conversion and an arbitrary subtype relation. Furthermore it
is shown that unification with respect to any subtype relation is
universal.
The paper is here.

Zhenyu Qian