Cartesian closed categories (CCCs) have played and continue to play an
important role in the study of the semantics of programming languages
. An axiomatization of the isomorphisms which hold in ail Cartesian cl
osed categories discovered independently by Soloviev and Bruce, Di Cos
mo and Longo leads to seven equalities. We show that the unification p
roblem for this theory is undecidable, thus settling an open question,
We also show that an important subcase, namely unification modulo the
linear isomorphisms, is NP-complete. Furthermore, the problem of matc
hing in CCCs is NP-complete when the subject term is irreducible. CCC-
matching and unification form the basis for an elegant and practical s
olution to the problem of retrieving functions from a library indexed
by types investigated by Rittri. It also has potential applications to
the problem of polymorphic type inference and polymorphic higher-orde
r unification, which in turn is relevant to theorem proving and logic
programming.