January 1995, 13pp.
Motivated by the problems of the undecidability of higher-order unification and hence the undecidability of lambda-Pi-unification, Pym and Elliott give a weaker notion of typing for lambda-Pi-objects: type similarity. In this paper we present a new calculus giving a formal theory of type similarity that captures this weaker notion of typing. We then apply a variant of Hardin's interpretation method to show that well-typed terms of this new calculus are confluent and normalizing for beta-eta-reduction. This is done by defining two translations of the new calculus into the lambda-Pi-calculus. We then use the results that well-typed lambda-Pi-terms are confluent and strongly normalizing to get our results.