constructive mathematics, realizability, computability
propositions as types, proofs as programs, computational trinitarianism
quantum algorithms:
Quantum computation is computation in terms of quantum information theory, possibly implemented on quantum computers, hence on physical systems for which phenomena of quantum mechanics are not negligible. In terms of computational trinitarianism quantum computation is the computation corresponding to (some kind of) quantum logic.
Specifically, topological quantum computation is (or is meant to be) quantum computation implemented on physical systems governed by topological quantum field theory, such as Chern-Simons theory. A prominent example of this is the (fractional) quantum Hall effect in solid state physics.
There are arguments that a good formal context for quantum computing is (via computational trinitarianism) linear logic/linear type theory (e.g. Lago-Faffian 12). See also at quantum logic.
The idea of quantum computation was first expressed in:
Paul Benioff, The computer as a physical system: A microscopic quantum mechanical Hamiltonian model of computers as represented by Turing machines, J Stat Phys 22, 563–591 (1980) (doi:10.1007/BF01011339)
Richard Feynman, Simulating physics with computers, Int J Theor Phys 21, 467–488 (1982) (doi:10.1007/BF02650179)
It became a plausible practical possibility with the understanding of quantum error correction in
Peter W. Shor, Scheme for reducing decoherence in quantum computer memory, Phys. Rev. A 52, R2493(R) 1995 (doi:10.1103/PhysRevA.52.R2493)
Andrew M. Steane, Error Correcting Codes in Quantum Theory, Phys. Rev. Lett. 77, 793 1996 (doi:10.1103/PhysRevLett.77.793)
Robert Calderbank, Peter W. Shor, Good Quantum Error-Correcting Codes Exist, Phys. Rev. A, Vol. 54, No. 2, pp. 1098-1106, 1996 (doi:10.1103/PhysRevA.54.1098)
Introduction and survey:
Michael A. Nielsen, Isaac L. Chuang, Quantum computation and quantum information, Cambridge University Press 2000 (pdf)
John Preskill, Quantum Computation lecture notes, since 2004 (web)
Jens Eisert, M. M. Wolf, Quantum computing, In: Handbook of Nature-Inspired and Innovative Computing, Springer 2006 (arXiv:quant-ph/0401019)
Greg Kuperberg, A concise introduction to quantum probability, quantum mechanics, and quantum computation, 2005 (pdf)
Michael Loceff, A course in quantum computing, 2013 (pdf)
Wikipedia, Quantum computation
Scott Aaronson, Lecture notes Quantum Computing Since Democritus 2006 (web)
National Academies of Sciences, Engineering, and Medicine, Quantum Computing: Progress and Prospects, The National Academies Press 2019 (doi:10.17226/25196)
On quantum programming languages (programming languages for quantum computation):
General:
Survey:
functional programming languages for quantum computation:
QPL:
Peter Selinger, The Quipper Language (web)
Alexander Green, Peter LeFanu Lumsdaine, Neil Ross, Peter Selinger, Benoît Valiron, Quipper: A Scalable Quantum Programming Language, ACM SIGPLAN Notices 48(6):333-342, 2013 (arXiv:1304.3390)
Alexander Green, Peter LeFanu Lumsdaine, Neil Ross, Peter Selinger, Benoît Valiron, An Introduction to Quantum Programming in Quipper, Lecture Notes in Computer Science 7948:110-124, Springer, 2013 (arXiv:1304.5485)
Jonathan Smith, Neil Ross, Peter Selinger, Benoît Valiron, Quipper: Concrete Resource Estimation in Quantum Algorithms, QAPL 2014 (arXiv:1412.0625)
Francisco Rios, Peter Selinger, A Categorical Model for a Quantum Circuit Description Language, EPTCS 266, 2018, pp. 164-178 (arXiv:1706.02630)
QML:
Thorsten Altenkirch, Jonathan Grattage, A functional quantum programming language, Logic in Computer Science, 2005. Proceedings. 20th Annual IEEE Symposium on, 26-29 June 2005 Page(s):249 - 258 (arXiv:quant-ph/0409065, doi:10.1109/LICS.2005.1, pdf)
Jonathan Grattage, An overview of QML with a concrete implementation in Haskell, Quantum Physics and Logic 2008 (arXiv:0806.2735)
Quantum programming via dependent linear type theory/indexed monoidal (∞,1)-categories:
Urs Schreiber, Quantization via Linear Homotopy Types (arXiv:1402.7041)
Peng Fu, Kohei Kishida, Peter Selinger, Linear Dependent Type Theory for Quantum Programming Languages, LICS ‘20: Proceedings of the 35th Annual ACM/IEEE Symposium on Logic in Computer ScienceJuly 2020 Pages 440–453 (arXiv:2004.13472, doi:10.1145/3373718.3394765, pdf, video)
specifically with Quipper:
On quantum software verification:
with Quipper:
Discussion of aspects of quantum programming in terms of monads in functional programming are in
Thorsten Altenkirch, Alexander Green, The quantum IO monad, in Semantic Techniques in Quantum Computation, January 2009, appeared in 2010 (pdf, talk slides)
J. K. Vizzotto, Thorsten Altenkirch, A. Sabry, Structuring quantum effects: superoperators as arrows (arXiv:quant-ph/0501151)
Discussion of quantum computation as the internal linear logic/linear type theory of compact closed categories is in
Samson Abramsky, Ross Duncan, A Categorical Quantum Logic, Mathematical Structures in Computer Science, 2006 (arXiv:quant-ph/0512114)
Ross Duncan, Types for quantum mechanics, 2006 (pdf, slides)
Ugo Dal Lago, Claudia Faggian, On Multiplicative Linear Logic, Modality and Quantum Circuits (arXiv:1210.0613)
An exposition along these lines is in
Discussion in terms of finite quantum mechanics in terms of dagger-compact categories:
topological quantum computation is discussed in
Michael Freedman, Alexei Kitaev, Michael J. Larsen, Zhenghan Wang, Topological Quantum Computation (arXiv:quant-ph/0101025)
Zhenghan Wang, Topologization of electron liquids with Chern-Simons theory and quantum computation (arXiv:cond-mat/0601285)
Michael Freedman, Michael Larsen, Zhenghan Wang, A modular functor which is universal for quantum computation (arXiv:quant-ph/0001108)
Alexei Kitaev, Fault-tolerant quantum computation by anyons, Annals Phys. 303 (2003) 2-30 (arXiv:quant-ph/9707021)
Relation to tensor networks, specifically matrix product states:
Last revised on May 7, 2021 at 11:43:48. See the history of this page for a list of all contributions to it.