Compiler correctness proofs
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).