@inproceedings(Maple-PVS:TPHOLS01,
 author       = "Andrew Adams and Martin Dunstan and Hanne Gottliebsen and Tom Kelsey and Ursula Martin and Sam Owre",
 year         = "2001",
 title        = "Computer Algebra Meets Automated Theorem Proving: Integrating {Maple} and {PVS}",
 editor       = "Richard J. Boulton and Paul B. Jackson",
 booktitle    = "Theorem Proving in Higher Order Logics, TPHOLs 2001",
 series       = "Lecture Notes in Computer Science",
 volume       = "2152",
 publisher    = "Springer-Verlag",
 address      = "Edinburgh, Scotland",
 pages        = "27--42",
 doi          = "10.1007/3-540-44755-5\_4",
)
@article(AkPa:metitarski,
 author       = "Behzad Akbarpour and Lawrence Charles Paulson",
 year         = "2010",
 title        = "MetiTarski: An Automatic Theorem Prover for Real-Valued Special Functions",
 journal      = "Journal of Automated Reasoning",
 volume       = "44",
 pages        = "175--205",
 doi          = "10.1007/s10817-009-9149-2",
)
@article(GaKa:acl2r,
 author       = "R. Gamboa and M. Kaufmann",
 year         = "2001",
 title        = "Nonstandard analysis in {ACL2}",
 journal      = "Journal of Automated Reasoning",
 volume       = "27",
 number       = "4",
 pages        = "323--351",
 doi          = "10.1023/A:1011908113514",
)
@phdthesis(Har:phd,
 author       = "J. Harrison",
 year         = "1996",
 title        = "Theorem Proving with the Real Numbers",
 school       = "University of Cambridge",
)
@inproceedings(KaFr:cas-hol,
 author       = "Cezary Kaliszyk and Freek Wiedijk",
 year         = "2007",
 title        = "Certified Computer Algebra on Top of an Interactive Theorem Prover",
 booktitle    = "Proceedings of the 14th symposium on Towards Mechanized Mathematical Assistants: 6th International Conference",
 series       = "Calculemus '07 / MKM '07",
 publisher    = "Springer-Verlag",
 address      = "Berlin, Heidelberg",
 pages        = "94--105",
 doi          = "10.1007/978-3-540-73086-6\_8",
)
@article(KM:ACL2-industrial,
 author       = "M. Kaufmann and {J S}. Moore",
 year         = "1997",
 title        = "An Industrial Strength Theorem Prover for a Logic Based on {C}ommon {L}isp",
 journal      = "IEEE Transactions on Software Engineering",
 volume       = "23",
 number       = "4",
 pages        = "203--213",
 doi          = "10.1109/32.588534",
)
@book(McMahon:quantum-computing,
 author       = "David McMahon",
 year         = "2008",
 title        = "Quantum Computing Explained",
 publisher    = "Wiley \& Sons",
)
@misc(Vazirani:quantum-notes,
 author       = "Umesh V. Vazirani",
 year         = "2012",
 title        = "Course Notes for Quantum Mechanics and Quantum Computation",
 howpublished = "\url {https://www.edx.org/courses/BerkeleyX/CS191x/2013_Spring/about}, previously on \burl {www.coursera.org}",
)
@book(YaMa:quantum-computing,
 author       = "Noson S. Yanofsky and Mirco A. Mannucci",
 year         = "2008",
 title        = "Quantum Computing for Computer Scientists",
 publisher    = "Cambridge University Press",
 doi          = "10.1017/CBO9780511813887",
)