Maschinen-unabhängige Code-Erzeugung als semantikerhaltende beweisbare Programmtransformation | lit.salon