Laurence Rideau, Bernard P. Serpette, Xavier Leroy. Tilting at Windmills with Coq: Formal Verification of a Compilation Algorithm for Parallel Moves. Journal of Automated Reasoning, 40(4):307-326, 2008. [doi]
@article{RideauSL08,
title = {Tilting at Windmills with Coq: Formal Verification of a Compilation Algorithm for Parallel Moves},
author = {Laurence Rideau and Bernard P. Serpette and Xavier Leroy},
year = {2008},
doi = {10.1007/s10817-007-9096-8},
url = {http://dx.doi.org/10.1007/s10817-007-9096-8},
researchr = {https://researchr.org/publication/RideauSL08},
cites = {0},
citedby = {0},
journal = {Journal of Automated Reasoning},
volume = {40},
number = {4},
pages = {307-326},
}