In this paper we propose a new form of polymorphism for object-oriented lan
guages, called correspondence polymorphism It lies in a different dimension
than either parametric or subtype polymorphism. In correspondence polymorp
hism, some methods are declared to correspond to other methods, via a corre
spondence relation. With this relation, it is possible to reuse non-generic
code in various type contexts-not necessarily subtyping or matching contex
ts-without having to plan ahead for this reuse. Correspondence polymorphism
has advantages over other expressive object type systems in that programme
r-declared types still may be simple, first-order types that are easily und
erstood. We define a simple language LCP that reflects these new ideas, ill
ustrating its behavior with multiple examples. We present formal type rules
and an operational semantics for LCP, and establish soundness of the type
system with respect to reduction.