VerifiedCompiler A compiler from a simple WHILE language to a Stack Machine assembly-like program. Proof of preservation of semantics is Lemma' found in Proofs.VerifiedCompilation.