H. Stoyan: Maschinen-unabhängige Code-Erzeugung als semantikerhaltende beweisbare Programmtransformation, 1984