1. Matthew Amy, Parsiad Azimzadeh & Michele Mosca (2018): On the controlled-NOT complexity of controlled-NOTphase circuits. Quantum Science and Technology 4(1), pp. 015002, doi:10.1088/2058-9565/aad8ca. Available at
  2. Matthew Amy, Dmitri Maslov & Michele Mosca (2014): Polynomial-Time T-depth optimization of Clifford+T circuits via matroid partitioning. IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems 33(10), pp. 1476–1489, doi:10.1109/TCAD.2014.2341953. Available at
  3. Matthew Amy, Olivia Di Matteo, Vlad Gheorghiu, Michele Mosca, Alex Parent & John Schanck (2016): Estimating the cost of generic quantum pre-image attacks on SHA-2 and SHA-3. In: Proceedings of the 24th Conference on Selected Areas in Cryptography (SAC'16), pp. 317–337, doi:10.1007/978-3-319-69453-5_18. Available at
  4. Matthew Amy & Michele Mosca (2016): T-count optimization and Reed-Muller codes. Available at
  5. Matthew Amy, Martin Roetteler & Krysta M. Svore (2017): Verified Compilation of Space-Efficient Reversible Circuits. In: Proceedings of the 29th International Conference on Computer Aided Verification (CAV'17), pp. 3–21, doi:10.1007/978-3-319-63390-9_1. Available at
  6. Linda Anticoli, Carla Piazza, Leonardo Taglialegne & Paolo Zuliani (2016): Towards Quantum Programs Verification: From Quipper Circuits to QPMC. In: Proceedings of the 8th international Conference on Reversible Computation (RC'16), pp. 213–219, doi:10.1007/978-3-319-40578-0_16. Available at
  7. Ebrahim Ardeshir-Larijani, Simon J. Gay & Rajagopal Nagarajan (2014): Verification of Concurrent Quantum Protocols by Equivalence Checking. In: Proceedings of the 20th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS'14), pp. 500–514, doi:10.1007/978-3-642-54862-8_42. Available at
  8. Dave Bacon, Wim van Dam & Alexander Russell (2008): Analyzing algebraic quantum circuits using exponential sums. Available at
  9. Filippo Bonchi, Fabio Gadducci, Aleks Kissinger, PawełSobociński & Fabio Zanasi (2016): Rewriting Modulo Symmetric Monoidal Structure. In: Proceedings of the 31st Annual ACM/IEEE Symposium on Logic in Computer Science, LICS '16, pp. 710–719, doi:10.1145/2933575.2935316. Available at
  10. Sergey Bravyi & David Gosset (2016): Improved Classical Simulation of Quantum Circuits Dominated by Clifford Gates. Physical Review Letters 116, pp. 250501, doi:10.1103/PhysRevLett.116.250501. Available at
  11. Bob Coecke, Ross Duncan, Aleks Kissinger & Quanlong Wang (2016): Generalised Compositional Theories and Diagrammatic Reasoning, pp. 309–366. Springer Netherlands, Dordrecht, doi:10.1007/978-94-017-7303-4_10. Available at
  12. Christopher M. Dawson, Andrew P. Hines, Duncan Mortimer, Henry L. Haselgrove, Michael A. Nielsen & Tobias J. Osborne (2005): Quantum computing and polynomial equations over Z_2. Quantum Information and Computation 5(2), pp. 102–112, doi:10.26421/QIC5.2. Available at
  13. Ross Duncan & Maxime Lucas (2013): Verifying the Steane code with Quantomatic. In: Proceedings of the 10th International Conference on Quantum Physics and Logic (QPL'13) 171, pp. 33–49, doi:10.4204/EPTCS.171.4.
  14. Richard P. Feynman & Albert R. Hibbs (1965): Quantum mechanics and path integrals. McGraw-Hill.
  15. Liam Garvie & Ross Duncan (2017): Verifying the Smallest Interesting Colour Code with Quantomatic. In: Proceedings of the 14th International Conference on Quantum Physics and Logic (QPL'17) 266, pp. 147–163, doi:10.4204/EPTCS.266.10.
  16. Simon J. Gay, Rajagopal Nagarajan & Nikolaos Papanikolaou (2008): QMC: A Model Checker for Quantum Systems. In: Proceedings of the 20th International Conference on Computer Aided Verification (CAV'08), pp. 543–547, doi:10.1007/978-3-540-70545-1_51. Available at
  17. Daniel Gottesman & Isaac L. Chuang (1999): Demonstrating the viability of universal quantum computation using teleportation and single-qubit operations. Nature 402(6760), pp. 390393, doi:10.1038/46503. Available at
  18. Markus Grassl, Brandon Langenberg, Martin Roetteler & Rainer Steinwandt (2016): Applying Grover's Algorithm to AES: Quantum Resource Estimates. In: Proceedings of the 7th International Workshop on Post-Quantum Cryptography (PQCrypto'16), pp. 29–43, doi:10.1007/978-3-319-29360-8_3. Available at
  19. IARPA (2013): Quantum Computer Science. Available at
  20. Phillip Kaye, Raymond Laflamme & Michele Mosca (2007): An Introduction to Quantum Computing. Oxford University Press.
  21. Dax Enshan Koh, Mark D Penney & Robert W Spekkens (2017): Computing quopit Clifford circuit amplitudes by the sum-over-paths technique. Quantum Information and Computation 17(13&14), pp. 1081–1095, doi:10.26421/QIC17.13-14. Available at
  22. Xavier Leroy (2006): Formal Certification of a Compiler Back-end or: Programming a Compiler with a Proof Assistant. In: Proceedings of the 34th International Symposium on Principles of Programming Languages (POPL'06). ACM, pp. 42–54, doi:10.1145/1111037.1111042.
  23. Dmitri Maslov (2016): Advantages of using relative-phase Toffoli gates with an application to multiple control Toffoli optimization. Physical Review A 93, pp. 022311, doi:10.1103/PhysRevA.93.022311. Available at
  24. Ashley Montanaro (2017): Quantum circuits and low-degree polynomials over F_2. Journal of Physics A: Mathematical and Theoretical 50(8), pp. 084002, doi:10.1088/1751-8121/aa565f. Available at
  25. Michael A. Nielsen & Isaac L. Chuang (2000): Quantum Computation and Quantum Information. Cambridge University Press.
  26. Ryan O'Donnell (2014): Analysis of Boolean Functions. Cambridge University Press, doi:10.1017/CBO9781139814782.
  27. Robert Rand, Jennifer Paykin & Steve Zdancewic (2017): QWIRE Practice: Formal Verification of Quantum Circuits in Coq. In: Proceedings of the 14th International Conference on Quantum Physics and Logic (QPL'17) 266, pp. 119–132, doi:10.4204/EPTCS.266.8.
  28. Martin Rötteler (2010): Quantum Algorithms for Highly Non-linear Boolean Functions. In: Proceedings of the 21st International Symposium on Discrete Algorithms (SODA'10), pp. 448–457, doi:10.1137/1.9781611973075.37. Available at
  29. Peter Selinger & Xiaoning Bian (2016): Relations for 2-qubit Clifford+T operator group. Available at
  30. Robert Wille, Daniel Grosse, D. Michael Miller & Rolf Drechsler (2009): Equivalence Checking of Reversible Circuits. In: Proceedings of the 39th International Symposium on Multiple-Valued Logic (ISMVL'09), pp. 324–330, doi:10.1109/ISMVL.2009.19.
  31. Shigeru Yamashita & Igor L. Markov (2010): Fast Equivalence-checking for Quantum Circuits. Quantum Information and Computation 10(9), pp. 721–734, doi:10.26421/QIC10.9-10. Available at
  32. Mingsheng Ying (2012): Floyd–Hoare Logic for Quantum Programs. ACM Transactions on Programming Languages and Systems 33(6), pp. 19:1–19:49, doi:10.1145/2049706.2049708. Available at

Comments and questions to:
For website issues: