natural deduction metalanguage, practical foundations
type theory (dependent, intensional, observational type theory, homotopy type theory)
computational trinitarianism =
propositions as types +programs as proofs +relation type theory/category theory
quantum algorithms:
constructive mathematics, realizability, computability
propositions as types, proofs as programs, computational trinitarianism
A quantum programming language is a programming language for quantum computation.
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:
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)
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) (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, Volume 16, Issue 3 (2006) pp. 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, pp. 55-66 (arXiv:1210.0613)
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)
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, talk at Quantum Physics and Logic 2008, ENTCS: Proceedings of QPL V - DCV IV, 157-165, Reykjavik, Iceland, 2008 (arXiv:0806.2735)
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 LanguagesJanuary 2017 Pages 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)
On classically controlled quantum computation:
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:
with QWIRE:
Last revised on May 12, 2021 at 06:48:44. See the history of this page for a list of all contributions to it.