Compiler correctness proofs 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.)
You'll need to modernize the notation, but McCarthy and Painter's Correctness of a Compiler for Arithmetic Expressions is simple and good, and also of historical interest (since to the best of my knowledge it's the first paper on the subject).