Title: A predicative theory of machine languages and its application to compiler correctness