#### Reduction and Unification in Lambda Calculi with Subtypes

#### Tobias Nipkow, Zhenyu Qian

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.
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.

SpringerLink

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.