Challenges in Quantum Programming Languages (Invited Talk)
In this talk, I will give an overview of some recent progress and current challenges in the design of quantum programming languages. Unlike classical programs, which can in principle be debugged by stopping the program at critical moments and examining the contents of variables, quantum programs are not amenable to traditional debugging because the state of a quantum system cannot usually be examined in a meaningful way. Therefore, we need other methods for ensuring the correctness of quantum programs, such as formal verification. For this reason, I advocate the use of strongly typed, functional programming languages for quantum computing. As far as functional quantum programming languages are concerned, there is currently a relatively wide gap between theory and practice. On the one hand, we have languages with strong theoretical foundations, such as the quantum lambda calculus, which operate at a relatively low level of abstraction and lack many features that would be useful to practical quantum programmers. On the other hand, we have practical functional quantum programming languages such as Quipper, which is implemented as an embedded language in Haskell, has many high-level features, and has been used in large-scale projects, but lacks a theoretical basis and a strong type system [Green et al., 2013; Green et al., 2013; Green et al., 2013; Smith et al., 2014]. We have recently attempted to narrow this gap through a family of languages called Proto-Quipper, which are designed to offer Quipper-like features while having sound theoretical foundations [Ross, 2015; Rios and Selinger, 2018]. I will give an overview of Quipper and its most useful features, report on the progress we made with formalizing fragments of Quipper, and outline several of the still remaining challenges.
Quantum programming languages
Theory of computation~Quantum computation theory
Theory of computation~Program semantics
3:1-3:2
Invited Talk
Peter
Selinger
Peter Selinger
Dalhousie University, Halifax, Canada
https://orcid.org/0000-0003-3161-856X
10.4230/LIPIcs.FSCD.2018.3
Alexander Green, Peter LeFanu Lumsdaine, Neil J. Ross, Peter Selinger, and Benoît Valiron. An introduction to quantum programming in Quipper. In Proceedings of the 5th International Conference on Reversible Computation, RC 2013, Victoria, British Columbia, volume 7948 of Lecture Notes in Computer Science, pages 110-124. Springer, 2013. Also available from https://arxiv.org/abs/1304.5485. URL: http://dx.doi.org/10.1007/978-3-642-38986-3_10.
http://dx.doi.org/10.1007/978-3-642-38986-3_10
Alexander Green, Peter LeFanu Lumsdaine, Neil J. Ross, Peter Selinger, and Benoît Valiron. Quipper: a scalable quantum programming language. In Proceedings of the 34th Annual ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2013, Seattle, volume 48(6) of ACM SIGPLAN Notices, pages 333-342, 2013. Also available from https://arxiv.org/abs/1304.3390. URL: http://dx.doi.org/10.1145/2499370.2462177.
http://dx.doi.org/10.1145/2499370.2462177
Alexander Green, Peter LeFanu Lumsdaine, Neil J. Ross, Peter Selinger, and Benoît Valiron. The Quipper language. Software implementation, available from http://www.mathstat.dal.ca/~selinger/quipper/, 2013.
http://www.mathstat.dal.ca/~selinger/quipper/
Francisco Rios and Peter Selinger. A categorical model for a quantum circuit description language. Extended abstract. In Proceedings of the 14th International Workshop on Quantum Physics and Logic, QPL 2017, Nijmegen, volume 266 of Electronic Proceedings in Theoretical Computer Science, pages 164-178. Open Publishing Association, 2018. Also available from https://arxiv.org/abs/1308.4557. URL: http://dx.doi.org/10.4204/EPTCS.266.11.
http://dx.doi.org/10.4204/EPTCS.266.11
Neil J. Ross. Algebraic and Logical Methods in Quantum Computation. PhD thesis, Department of Mathematics and Statistics, Dalhousie University, 2015. Available from URL: https://arxiv.org/abs/1510.02198.
https://arxiv.org/abs/1510.02198
Jonathan M. Smith, Neil J. Ross, Peter Selinger, and Benoît Valiron. Quipper: concrete resource estimation in quantum algorithms. Extended abstract for a talk given at the 12th International Workshop on Quantitative Aspects of Programming Languages and Systems, QAPL 2014, Grenoble. Available from https://arxiv.org/abs/1412.0625, 2014.
https://arxiv.org/abs/1412.0625
Peter Selinger
Creative Commons Attribution 3.0 Unported license
https://creativecommons.org/licenses/by/3.0/legalcode