@article(aam17,
 author       = {Matthew Amy and Parsiad Azimzadeh and Michele Mosca},
 year         = {2018},
 title        = {{On the controlled-NOT complexity of controlled-NOT\IeC{\textendash}phase circuits}},
 journal      = {Quantum Science and Technology},
 volume       = {4},
 number       = {1},
 pages        = {015002},
 doi          = {10.1088/2058-9565/aad8ca},
 url          = {https://arxiv.org/abs/1712.01859},
)
@article(amm14,
 author       = {Matthew Amy and Dmitri Maslov and Michele Mosca},
 year         = {2014},
 title        = {{Polynomial-Time {T}-depth optimization of {C}lifford+{T} circuits via matroid partitioning}},
 journal      = {IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems},
 volume       = {33},
 number       = {10},
 pages        = {1476--1489},
 doi          = {10.1109/TCAD.2014.2341953},
 url          = {https://arxiv.org/abs/1303.2042},
)
@inproceedings(adgmps16,
 author       = {Matthew Amy and Olivia~Di Matteo and Vlad Gheorghiu and Michele Mosca and Alex Parent and John Schanck},
 year         = {2016},
 title        = {{Estimating the cost of generic quantum pre-image attacks on SHA-2 and SHA-3}},
 booktitle    = {Proceedings of the 24th Conference on Selected Areas in Cryptography (SAC'16)},
 pages        = {317--337},
 doi          = {10.1007/978-3-319-69453-5_18},
 url          = {https://arxiv.org/abs/1603.09383},
)
@misc(am16,
 author       = {Matthew Amy and Michele Mosca},
 year         = {2016},
 title        = {{T-count optimization and Reed-Muller codes}},
 url          = {https://arxiv.org/abs/1601.07363},
)
@inproceedings(ars17,
 author       = {Matthew Amy and Martin Roetteler and Krysta~M. Svore},
 year         = {2017},
 title        = {{Verified Compilation of Space-Efficient Reversible Circuits}},
 booktitle    = {Proceedings of the 29th International Conference on Computer Aided Verification (CAV'17)},
 pages        = {3--21},
 doi          = {10.1007/978-3-319-63390-9_1},
 url          = {https://arxiv.org/abs/1603.01635},
)
@inproceedings(z16,
 author       = {Linda Anticoli and Carla Piazza and Leonardo Taglialegne and Paolo Zuliani},
 year         = {2016},
 title        = {{Towards Quantum Programs Verification: From Quipper Circuits to QPMC}},
 booktitle    = {Proceedings of the 8th international Conference on Reversible Computation (RC'16)},
 pages        = {213--219},
 doi          = {10.1007/978-3-319-40578-0_16},
 url          = {https://arxiv.org/abs/1708.06312},
)
@inproceedings(agn14,
 author       = {Ardeshir-Larijani, Ebrahim and Simon~J. Gay and Rajagopal Nagarajan},
 year         = {2014},
 title        = {{Verification of Concurrent Quantum Protocols by Equivalence Checking}},
 booktitle    = {Proceedings of the 20th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS'14)},
 pages        = {500--514},
 doi          = {10.1007/978-3-642-54862-8_42},
 url          = {https://arxiv.org/abs/1312.5951},
)
@misc(bvr08,
 author       = {Dave Bacon and Wim van Dam and Alexander Russell},
 year         = {2008},
 title        = {{Analyzing algebraic quantum circuits using exponential sums}},
 url          = {https://www.cs.ucsb.edu/~vandam/LeastAction.pdf},
)
@inproceedings(bgksz16,
 author       = {Filippo Bonchi and Fabio Gadducci and Aleks Kissinger and Pawe{\l} Soboci\'{n}ski and Fabio Zanasi},
 year         = {2016},
 title        = {{Rewriting Modulo Symmetric Monoidal Structure}},
 booktitle    = {Proceedings of the 31st Annual ACM/IEEE Symposium on Logic in Computer Science},
 series       = {LICS '16},
 pages        = {710--719},
 doi          = {10.1145/2933575.2935316},
 url          = {https://arxiv.org/abs/1602.06771},
)
@article(bg16,
 author       = {Sergey Bravyi and David Gosset},
 year         = {2016},
 title        = {{Improved Classical Simulation of Quantum Circuits Dominated by Clifford Gates}},
 journal      = {Physical Review Letters},
 volume       = {116},
 pages        = {250501},
 doi          = {10.1103/PhysRevLett.116.250501},
 url          = {https://arxiv.org/abs/1601.07601},
)
@inbook(cdkw16,
 author       = {Bob Coecke and Ross Duncan and Aleks Kissinger and Quanlong Wang},
 year         = {2016},
 title        = {{Generalised Compositional Theories and Diagrammatic Reasoning}},
 pages        = {309--366},
 publisher    = {Springer Netherlands},
 address      = {Dordrecht},
 doi          = {10.1007/978-94-017-7303-4_10},
 url          = {https://arxiv.org/abs/1506.03632},
)
@article(dhmhno05,
 author       = {Christopher~M. Dawson and Andrew~P. Hines and Duncan Mortimer and Henry~L. Haselgrove and Michael~A. Nielsen and Tobias~J. Osborne},
 year         = {2005},
 title        = {{Quantum computing and polynomial equations over {$\mathbb{Z}_2$}}},
 journal      = {Quantum Information and Computation},
 volume       = {5},
 number       = {2},
 pages        = {102--112},
 doi          = {10.26421/QIC5.2},
 url          = {https://arxiv.org/abs/quant-ph/0408129},
)
@inproceedings(dl13,
 author       = {Ross Duncan and Maxime Lucas},
 year         = {2013},
 title        = {{Verifying the Steane code with Quantomatic}},
 booktitle    = {Proceedings of the 10th International Conference on Quantum Physics and Logic (QPL'13)},
 volume       = {171},
 pages        = {33--49},
 doi          = {10.4204/EPTCS.171.4},
)
@book(fh65,
 author       = {Richard~P. Feynman and Albert~R. Hibbs},
 year         = {1965},
 title        = {Quantum mechanics and path integrals},
 publisher    = {McGraw-Hill},
)
@inproceedings(gd17,
 author       = {Liam Garvie and Ross Duncan},
 year         = {2017},
 title        = {{Verifying the Smallest Interesting Colour Code with Quantomatic}},
 booktitle    = {Proceedings of the 14th International Conference on Quantum Physics and Logic (QPL'17)},
 volume       = {266},
 pages        = {147--163},
 doi          = {10.4204/EPTCS.266.10},
)
@inproceedings(gnp08,
 author       = {Simon~J. Gay and Rajagopal Nagarajan and Nikolaos Papanikolaou},
 year         = {2008},
 title        = {{QMC: A Model Checker for Quantum Systems}},
 booktitle    = {Proceedings of the 20th International Conference on Computer Aided Verification (CAV'08)},
 pages        = {543--547},
 doi          = {10.1007/978-3-540-70545-1_51},
 url          = {https://arxiv.org/abs/0704.3705},
)
@article(gc99,
 author       = {Daniel Gottesman and Isaac~L. Chuang},
 year         = {1999},
 title        = {{Demonstrating the viability of universal quantum computation using teleportation and single-qubit operations}},
 journal      = {Nature},
 volume       = {402},
 number       = {6760},
 pages        = {390\IeC{\textendash}393},
 doi          = {10.1038/46503},
 url          = {https://arxiv.org/abs/quant-ph/9908010},
)
@inproceedings(glrs16,
 author       = {Markus Grassl and Brandon Langenberg and Martin Roetteler and Rainer Steinwandt},
 year         = {2016},
 title        = {{Applying Grover's Algorithm to AES: Quantum Resource Estimates}},
 booktitle    = {Proceedings of the 7th International Workshop on Post-Quantum Cryptography (PQCrypto'16)},
 pages        = {29--43},
 doi          = {10.1007/978-3-319-29360-8_3},
 url          = {https://arxiv.org/abs/1512.04965},
)
@misc(IARPAQCS,
 author       = {IARPA},
 year         = {2013},
 title        = {Quantum Computer Science},
 url          = {https://www.iarpa.gov/index.php/research-programs/qcs/baa},
)
@book(klm07,
 author       = {Phillip Kaye and Raymond Laflamme and Michele Mosca},
 year         = {2007},
 title        = {An Introduction to Quantum Computing},
 publisher    = {Oxford University Press},
)
@article(kps17,
 author       = {Dax~Enshan Koh and Mark~D Penney and Robert~W Spekkens},
 year         = {2017},
 title        = {{Computing quopit Clifford circuit amplitudes by the sum-over-paths technique}},
 journal      = {Quantum Information and Computation},
 volume       = {17},
 number       = {13\&14},
 pages        = {1081--1095},
 doi          = {10.26421/QIC17.13-14},
 url          = {https://arxiv.org/abs/1702.03316},
)
@inproceedings(l06,
 author       = {Xavier Leroy},
 year         = {2006},
 title        = {{Formal Certification of a Compiler Back-end or: Programming a Compiler with a Proof Assistant}},
 booktitle    = {Proceedings of the 34th International Symposium on Principles of Programming Languages (POPL'06)},
 publisher    = {ACM},
 pages        = {42--54},
 doi          = {10.1145/1111037.1111042},
)
@article(m16,
 author       = {Dmitri Maslov},
 year         = {2016},
 title        = {{Advantages of using relative-phase Toffoli gates with an application to multiple control Toffoli optimization}},
 journal      = {Physical Review A},
 volume       = {93},
 pages        = {022311},
 doi          = {10.1103/PhysRevA.93.022311},
 url          = {https://arxiv.org/abs/1508.03273},
)
@article(m17,
 author       = {Ashley Montanaro},
 year         = {2017},
 title        = {{Quantum circuits and low-degree polynomials over ${{\mathbb{F}}_\mathsf{2}}$}},
 journal      = {Journal of Physics A: Mathematical and Theoretical},
 volume       = {50},
 number       = {8},
 pages        = {084002},
 doi          = {10.1088/1751-8121/aa565f},
 url          = {https://arxiv.org/abs/1607.08473},
)
@book(nc00,
 author       = {Michael~A. Nielsen and Isaac~L. Chuang},
 year         = {2000},
 title        = {{Quantum Computation and Quantum Information}},
 publisher    = {Cambridge University Press},
)
@book(od14,
 author       = {Ryan O'Donnell},
 year         = {2014},
 title        = {{Analysis of Boolean Functions}},
 publisher    = {Cambridge University Press},
 doi          = {10.1017/CBO9781139814782},
)
@inproceedings(rpz18,
 author       = {Robert Rand and Jennifer Paykin and Steve Zdancewic},
 year         = {2017},
 title        = {{QWIRE Practice: Formal Verification of Quantum Circuits in Coq}},
 booktitle    = {Proceedings of the 14th International Conference on Quantum Physics and Logic (QPL'17)},
 volume       = {266},
 pages        = {119--132},
 doi          = {10.4204/EPTCS.266.8},
)
@inproceedings(r10,
 author       = {Martin R\"{o}tteler},
 year         = {2010},
 title        = {{Quantum Algorithms for Highly Non-linear Boolean Functions}},
 booktitle    = {Proceedings of the 21st International Symposium on Discrete Algorithms (SODA'10)},
 pages        = {448--457},
 doi          = {10.1137/1.9781611973075.37},
 url          = {https://arxiv.org/abs/0811.3208},
)
@misc(bs16,
 author       = {Peter Selinger and Xiaoning Bian},
 year         = {2016},
 title        = {{Relations for 2-qubit {C}lifford+{T} operator group}},
 url          = {https://www.mathstat.dal.ca/~xbian/talks/slide_cliffordt2.pdf},
)
@inproceedings(w09,
 author       = {Robert Wille and Daniel Grosse and D.~Michael Miller and Rolf Drechsler},
 year         = {2009},
 title        = {{Equivalence Checking of Reversible Circuits}},
 booktitle    = {Proceedings of the 39th International Symposium on Multiple-Valued Logic (ISMVL'09)},
 pages        = {324--330},
 doi          = {10.1109/ISMVL.2009.19},
)
@article(y10,
 author       = {Shigeru Yamashita and Igor~L. Markov},
 year         = {2010},
 title        = {{Fast Equivalence-checking for Quantum Circuits}},
 journal      = {Quantum Information and Computation},
 volume       = {10},
 number       = {9},
 pages        = {721--734},
 doi          = {10.26421/QIC10.9-10},
 url          = {https://arxiv.org/abs/0909.4119},
)
@article(y12,
 author       = {Mingsheng Ying},
 year         = {2012},
 title        = {{Floyd--Hoare Logic for Quantum Programs}},
 journal      = {ACM Transactions on Programming Languages and Systems},
 volume       = {33},
 number       = {6},
 pages        = {19:1--19:49},
 doi          = {10.1145/2049706.2049708},
 url          = {https://arxiv.org/abs/0906.4586},
)