Een theorie van data strukturen voor de informatika hoort aan zekere eisen te voldoen. Zij moet een notatie voor het definiëeren van nieuwe data strukturen aanbieden, alsmede een leidraad voor het schrijven van rekursieve funkties die op de gedefiniëeerde typen opereren. Vooral is het van belang dat de notatie voor deze funkties goed formeel hanteerbaar is. Het is immers dikwijls het gemakkelijkst om een evident korrekt programma te schrijven terwijl de efficiëntie van dit programma veel te wensen overlaat. Daarom is het nuttig programma's te kunnen transformeren op zo'n manier dat de korrektheid gehandhaafd wordt en de efficiëntie verbeterd. Kortom, een theorie van data strukturen moet ook een calculus voor het transformeren van programma's bevatten.
In dit proefschrift wordt een notatie voor het definiëren van data typen dmv zogenaamde initiële algebra's besproken. Deze notatie berust op een unieke extensie eigenschap. Deze vormt zowel een manier om rekursieve funkties te schrijven als de basis voor een calculus voor programma transformatie. De unieke extensie eigenschap, en een gevolg daarvan, de zogenaamde ,,promotie stelling'', lenen zich goed voor het uitvoeren van korte en fraaie programma transformaties. De notatie en enkele voorbeelden worden in het tweede hoofdstuk uiteengezet. Het derde hoofdstuk behandelt een eenvoudige uitbreiding van de notatie om ook data typen met oneindige elementen te kunnen definiëren, bv het type van oneindige rijen. Het vierde hoofdstuk gaat over het gebruik van relaties ipv funkties bij het afleiden en transformeren van programma's die op subtypen opereren. Hier speelt zowel de algebraische als de logische struktuur van het data type een belangrijke rol. Het vijfde hoofdstuk behandelt het bestaan van de gedefiniëerde typen. Geparametriseerde typen worden in het tweede en derde hoofdstuk besproken: daar wordt getoond dat ze een manier vormen om nieuwe typen te definiëren. Er wordt bewezen dat de zo gedefiniëerde typen bestaan.