Motivated by the desire to prove imnlementations correct, we present two approaches to making
the fundamental notion of implementation as a relationship between data types precise. The
first one captures the idea of simulation, while the second one, being more constructive in
nature, formalizes the idea of constructing on a given basis in distinguished steps something
isomorphic to a given target structure. Both approaches give rise to corresponding proof
methods which are demonstrated in examples. The approaches are shown to be equivalent as
far as the existence of implementations is concerned.