  This paper describes an ACL2 interpreter for "netlists" describing quantum
circuits. Several quantum gates are implemented, including the Hadamard gate H,
which rotates vectors by 45 degrees, necessitating the use of irrational
numbers, at least at the logical level. Quantum measurement presents an
especially difficult challenge, because it requires precise comparisons of
irrational numbers and the use of random numbers. This paper does not address
computation with irrational numbers or the generation of random numbers,
although future work includes the development of pseudo-random generators for
ACL2.

Logic in Computer Science;Quantum Physics