nLab quantum programming languages -- 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, talk slides: pdf, pdf $]$

(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)