Extending Coq with Imperative Features and Its Application to SAT Verification.

Michal Armand, Benjamin Grgoire, Arnaud Spiwack, Laurent Thry

Browse the full ITP paper archive.