I am looking for tutorial material that covers compiler correctness proofs, preferably using denotational methods, at the level of a beginning grad student.  Alternatively, do you know of some simple compiler examples that I could use to illustrate the issues?  (The first example that occurred to me was a translator from infix to postfix expressions.  But it failed to show anything interesting other than how to do induction on syntax.)
Compiler correctness proofs
reference request;pl.programming languages;semantics;compilers
I do not know of good tutorial material, but there are papers that are sufficiently elementary for a grad student (like me). The first might be what you are looking for (emphasis is mine).Simple relational correctness proofs for static analyses and program transformations, Nick Benton. 2004.We show how some classical static analyses for imperative programs, and the optimizing transformations which they enable, may be expressed and proved correct using elementary logical and denotational techniques. The key ingredients are an interpretation of program properties as relations, rather than predicates, and a realization that although many program analyses are traditionally formulated in very intensional terms, the associated transformations are actually enabled by more liberal extensional properties.These papers may also interest you. They helped me greatly!Proving Correctness of Compiler Optimizations by Temporal Logic, David Lacey, Neil D. Jones, Eric Van Wyk, Carl Christian Frederiksen. I would have thought there was more material using bisimulation in the context of compiler optimizations. If your aim is really denotational techniques, you can probably encode these proofs using characterisations of bisimulation.Generating Compiler Optimizations from Proofs, Ross Tate, Michael Stepp, and Sorin Lerner. Includes a category theoretic formalisation of their proof method.Proving Optimizations Correct using Parameterized Program Equivalence, Sudipta Kundu, Zachary Tatlock, and Sorin Lerner. Go there if you like logical relations.A Formally Verified Compiler Back-end Xavier Leroy.