Using domain algebras to prove the correctness of a compiler