Proof Object Transformation, Preserving Imp Embeddings: the first proof compiler to be formally proven correct - View it on GitHub