Abstract
This thesis extends the study of the notion of termination equivalence of abstract structures first proposed by Kfoury. The connection with abstract data types (ADTs) is made by demonstrating that many kinds of equivalence between ADT implementations are in fact instances of termination equivalence between their underlying algebras. The results in the thesis extend the original work in two directions. The first is to consider how the termination equivalence of structures is dependent upon the choice of programming formalism. The termination equivalences for all of the common classes of programs and for some new classes of non-computable schemes are studied, and their relative strengths are established. The other direction is a study of a congruence property of equivalences relative to the join or addition datatype building operation. We decide which of the termination equivalences are congruences for all structures and for all computable structures, and for those equivalences which are not, we characterise those congruences closest to them (both stronger and weaker). These programmes of work involved the use of constructions and properties of structures relating to program termination which are of interest in themselves. These are examined and are used to prove some general results about the relative strengths of termination equivalences.