Proving a compiler correct: A simple approach
scientific article; zbMATH DE number 3476565