An Interpreter for Quantum Circuits - Lucas Helms; Ruben Gamboa (ACL2, 2013)