Towards Proof Generating Compilers

The paper describes the overall approach and applies it to a simple translation scenario. Specification and verification is done within the theorem prover Isabelle/HOL. To show the flexibility of the approach, we present two different proof techniques for translation correctness.