Challenges in Quantum Programming Languages (Invited Talk)

Author Peter Selinger

Thumbnail PDF


  • Filesize: 213 kB
  • 2 pages

Document Identifiers

Author Details

Peter Selinger
  • Dalhousie University, Halifax, Canada

Cite AsGet BibTex

Peter Selinger. Challenges in Quantum Programming Languages (Invited Talk). In 3rd International Conference on Formal Structures for Computation and Deduction (FSCD 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 108, pp. 3:1-3:2, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)


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.

Subject Classification

ACM Subject Classification
  • Theory of computation → Quantum computation theory
  • Theory of computation → Program semantics
  • Quantum programming languages


  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    PDF Downloads


  1. 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 URL:
  2. 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 URL:
  3. Alexander Green, Peter LeFanu Lumsdaine, Neil J. Ross, Peter Selinger, and Benoît Valiron. The Quipper language. Software implementation, available from, 2013.
  4. 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 URL:
  5. Neil J. Ross. Algebraic and Logical Methods in Quantum Computation. PhD thesis, Department of Mathematics and Statistics, Dalhousie University, 2015. Available from URL:
  6. 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, 2014.
Questions / Remarks / Feedback

Feedback for Dagstuhl Publishing

Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail