Tilting at Windmills with Coq: Formal Verification of a Compilation Algorithm for Parallel Moves