nLab quantum programming language

Idea

A quantum programming language is a programming language for quantum computation.

In as far as data types in classical programming languages may and often are understood in terms of (dependent) type theory, quantum programming languages concern quantum data types such as “qbits” which may be understood via linear logic (Pratt (1992)) in (dependent) linear type theory (e.g. Abramsky & Duncan (2005); Duncan (2006); Dal Lago & Faggian (2012); Green et al (2013); Staton (2015)):

“A quantum programming language captures the ideas of quantum computation in a linear type theory.” [Staton (2015), p. 1]

Many existing quantum programming languages are in fact domain specific programming languages for the description of quantum circuits compiled from quantum logic gates, and as such often embedded into ambient type theories (eg. Quipper and QWIRE).

Other QPLs are more algorithmic (such as Q Sharp).

Related concepts

• programming language

• quantum logic

• quantum logic gate, quantum circuit

• linear logic, linear type theory, dependent linear type theory

References

Quantum programming languages

The first proposal towards formalizing quantum programming languages was:

• Emanuel Knill, Conventions for quantum pseudocode, Los Alamos Technical Report (1996) $[$LA-UR-96-2724, doi:10.2172/366453, pdf, pdf$]$

and early formalization via quantum lambda-calculus invoking linear logic/linear types (cf. Pratt 1992 etc.):

• Benoît Valiron, A functional programming language for quantum computation with classical control, MSc thesis, University of Ottawa (2004) $[$doi:10.20381/ruor-18372, pdf$]$

• Peter Selinger, Benoît Valiron, A lambda calculus for quantum computation with classical control, Proc. of TLCA 2005 $[$arXiv:cs/0404056, doi:10.1007/11417170_26$]$

• Peter Selinger, Benoît Valiron, Quantum Lambda Calculus, in: Semantic Techniques in Quantum Computation, Cambridge University Press (2009) 135-172 $[$doi:10.1017/CBO9781139193313.005, pdf$]$

[Selinger (2016):] When the QPL workshop series was first founded, it was called “Quantum Programming Languages”. One year I wasn’t participating, and while I wasn’t looking they changed the name to “Quantum Physics and Logic” — same acronym!

Back in those days in the early 21st century we were actually trying to do programming languages for quantum computing $[$Selinger & Valiron 2004$]$, but the sad thing is: In those days nobody really cared. $[...]$

Now it’s 15 years later and several of these parameters have changed: There has been a renewed interest, from government agencies and also from companies who are actually building quantum computers. $[...]$.

So now people are working on quantum programming languages again.

Exposition of the general idea of quantum programming languages for classically controlled quantum computation with an eye towards the Quipper-language:

• Benoît Valiron, Neil J. Ross, Peter Selinger, D. Scott Alexander, Jonathan M. Smith, Programming the quantum future, Communications of the ACM 58 8 (2015) 52–61 $[$doi:10.1145/2699415, pdf, web, promo vid:YT$]$

On quantum programming languages (programming languages for quantum computation):

General:

• Jarosław Adam Miszczak, Models of quantum computation and quantum programming languages, Bull. Pol. Acad. Sci.-Tech. Sci., Vol. 59, No. 3 (2011), pp. 305-324 (arXiv:1012.6035)

• Jarosław Adam Miszczak, High-level Structures for Quantum Computing, Morgan&Claypool 2012 (doi:10.2200/S00422ED1V01Y201205QMC006, pdf)

See also:

• Wikipedia, Quantum programming

Surveys of existing languages:

• Simon Gay, Quantum programming languages: Survey and bibliography, Mathematical Structures in Computer Science16(2006) (doi:10.1017/S0960129506005378, pdf)

• Sunita Garhwal, Maryam Ghorani , Amir Ahmad, Quantum Programming Language: A Systematic Review of Research Topic and Top Cited Languages, Arch Computat Methods Eng 28, 289–310 (2021) (doi:10.1007/s11831-019-09372-6)

• B. Heim et al., Quantum programming languages, Nat Rev Phys 2 (2020) 709–722 $[$doi:10.1038/s42254-020-00245-7$]$

Quantum programming via quantum logic understood as linear type theory interpreted in symmetric monoidal categories:

• Vaughan Pratt, Linear logic for generalized quantum mechanics, in Proc. of Workshop on Physics and Computation (PhysComp’92), Dallas (1992) $[$pdf, Pratt-LinearLogic.pdf, web$]$

• Samson Abramsky, Bob Coecke, A categorical semantics of quantum protocols , Proceedings of the 19th IEEE conference on Logic in Computer Science (LiCS’04). IEEE Computer Science Press (2004) (arXiv:quant-ph/0402130)

• Samson Abramsky, Ross Duncan, A Categorical Quantum Logic, Mathematical Structures in Computer Science, 16 3 (2006) 469-489 $[$arXiv:quant-ph/0512114, doi:10.1017/S0960129506005275$]$

• Ross Duncan, Types for Quantum Computing, (2006) $[$pdf$]$

• Ugo Dal Lago, Claudia Faggian, On Multiplicative Linear Logic, Modality and Quantum Circuits, EPTCS 95 (2012) 55-66 $[$arXiv:1210.0613, doi:10.4204/EPTCS.95.6$]$

• Sam Staton, Algebraic Effects, Linearity, and Quantum Programming Languages, POPL ‘15: Proceedings of the 42nd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (2015) $[$doi:10.1145/2676726.2676999, pdf$]$

  “A quantum programming language captures the ideas of quantum computation in a linear type theory.”

The corresponding string diagrams are known in quantum computation as quantum circuit diagrams:

• Giuliano Benenti, Giulio Casati, Davide Rossini, Chapter 3 of: Principles of Quantum Computation and Information, World Scientific 2018 (doi:10.1142/10909, 2004 pdf)

• Miszczak 12, Sec. 4.3

Typed$\;$functional programming languages for quantum computation:

QPL:

• Peter Selinger, Towards a quantum programming language, Mathematical Structures in Computer Science 14 4 (2004) 527–586 $[$doi:10.1017/S0960129504004256, pdf, web$]$

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, talk at Quantum Physics and Logic 2008, ENTCS: Proceedings of QPL V - DCV IV, 157-165, Reykjavik, Iceland, 2008 (arXiv:0806.2735)

quantum IO monad:

• Thorsten Altenkirch, Alexander Green, The quantum IO monad, Ch. 5 of: Simon Gay, Ian Mackie (eds.): Semantic Techniques in Quantum Computation (2010) 173-205 $[$pdf, doi:10.1017/CBO9781139193313.006$]$

Quipper:

• 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 (2013) 333-342 $[$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)

QWIRE:

• Jennifer Paykin, Robert Rand, Steve Zdancewic, QWIRE: a core language for quantum circuits, POPL 2017: Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages (2017) 846–858 (doi:10.1145/3009837.3009894)

  (using the exponential modality between linear type theory and intuitionistic type theory)

• Jennifer Paykin, Linear/non-Linear Types For Embedded Domain-Specific Languages, 2018 (upenn:2752)

• Jennifer Paykin, Steve Zdancewic, A HoTT Quantum Equational Theory, talk at QPL2019 (arXiv:1904.04371)

  (using ambient homotopy type theory)

CoqQ:

• Li Zhou, Gilles Barthe, Pierre-Yves Strub, Junyi Liu, Mingsheng Ying, CoqQ: Foundational Verification of Quantum Programs $[$arXiv:2207.11350$]$

On Q Sharp:

• Kartik Singhal, Kesha Hietala, Sarah Marshall, Robert Rand, Q# as a Quantum Algorithmic Language, Proceedings of Quantum Physics and Logic (2022) $[$arXiv:2206.03532$]$

On classically controlled quantum computation:

• Bernhard Ömer, Structured Quantum Programming, 2003/2009 (pdf)

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:

• Peng Fu, Kohei Kishida, Neil Ross, Peter Selinger, A Tutorial Introduction to Quantum Circuit Programming in Dependently Typed Proto-Quipper, in I. Lanese, M. Rawski (eds.) Reversible Computation RC 2020. Lecture Notes in Computer Science, vol 12227 (arXiv:2005.08396, doi:10.1007/978-3-030-52482-1_9)

See also QS.

On quantum software engineering:

• Manuel A. Serrano, Ricardo Pérez-Castillo, Mario Piattini, Quantum Software Engineering, Springer (2022) $[$doi:10.1007/978-3-031-05324-5$]$

On software verification:

with QWIRE:

• Robert Rand, Jennifer Paykin, Steve Zdancewic, QWIRE Practice: Formal Verification of Quantum Circuits in Coq, EPTCS 266, 2018, pp. 119-132 (arXiv:1803.00699)

• Robert Rand, Jennifer Paykin, Dong-Ho Lee, Steve Zdancewic, ReQWIRE: Reasoning about Reversible Quantum Circuits, EPTCS 287 (2019) 299-312 $[$arXiv:1901.10118, doi:10.4204/EPTCS.287.17$]$

for Quipper with QPMC:

• Linda Anticoli, Carla Piazza, Leonardo Taglialegne, Paolo Zuliani, Towards Quantum Programs Verification: From Quipper Circuits to QPMC, In: Devitt S., Lanese I. (eds.) Reversible Computation. RC 2016, Lecture Notes in Computer Science 9720 Springer (2016) $[$arXiv:1708.06312, doi:10.1007/978-3-319-40578-0_16$]$

with CoqQ: Ying et al. (2022)