The semantics of type definitions, declarations of structured
variables, assignment and evaluation is specified algebraically by means of
abstract data types. Corresponding proof rules are given which can be used
for program verification. Then, a unifying approach to the semantics of type
definitions is presented by giving an axiom system for a general algebra of
structured objects in which type definitions are represented by equations.
The structure of models for the axiom system and the solvability of these
equations is discussed.