Quipper (Rev #22, changes) in nLab

Showing changes from revision #21 to #22: Added | Removed | Changed

Contents

Idea

Quipper is a functional quantum programming language, specifically a domain specific programming language for quantum circuits which is embedded into Haskell. As such it is similar to QWIRE.

• QML

• QPL

References

General

Resources:

• Peter Selinger, The Quipper Language (web)

Precursor discussion:

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

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](https://doi.org/10.1145/2699415), pdf, web, promo vid:YT]

Original articles on Quipper:

• 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](https://arxiv.org/abs/1304.3390), doi:10.1145/2499370.2462177]

• Jonathan Smith, Neil Ross, Peter Selinger, Benoît Valiron, Quipper: Concrete Resource Estimation in Quantum Algorithms, QAPL 2014 (arXiv:1412.0625)

• Neil J. Ross, Chapters 8-9 in: Algebraic and Logical Methods in Quantum Computation, Ph.D. thesis, Dalhousie University (2015) [[arXiv:1510.02198](https://arxiv.org/abs/1510.02198)]

  (introducing Proto-Quipper)

Introduction and review:

• 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 Springer (2013) 110-124 [[arXiv:1304.5485](https://arxiv.org/abs/1304.5485), doi:10.1007/978-3-642-38986-3_10]

• Peter Selinger, Introduction to Quipper, talk at QPL2016 (2016) [[video](https://youtu.be/59frzb__Eqo)]

On quantum software verification for/with Quipper:

• 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, vol 9720. Springer, Cham (doi:10.1007/978-3-319-40578-0_16)

Dependent linear types and categorical semantics

Discussion of some dependent linear type theory and categorical semantics for (proto-)Quipper:

• Francisco Rios, Peter Selinger, A Categorical Model for a Quantum Circuit Description Language, EPTCS 266 (2018) 164-178 [[arXiv:1706.02630](https://arxiv.org/abs/1706.02630), doi:10.4204/EPTCS.266.11]

• 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](https://arxiv.org/abs/2005.08396), doi:10.1007/978-3-030-52482-1_9]

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

• Francisco Rios, On a Categorically Sound Quantum Programming Language for Circuit Description, Dalhousie University (2021) [[hdl:10222/80771](http://hdl.handle.net/10222/80771)]

• Dongho Lee, Formal Methods for Quantum Programming Languages, Paris Saclay (Dec 2022) [[hal:tel-03895847](https://hal.science/LMF/tel-03895847)]

Dynamic lifting

The issue of “dynamic lifting” (of “bits” resulting from quantum measurement back into the “context”):

• brief mentioning on GLRSV13, p. 5

• Robert Rand, Formally Verified Quantum Programming, UPenn (2018) [[ediss:3175](https://repository.upenn.edu/edissertations/3175)]

• Dongho Lee, Sebastien Bardin, Valentin Perrelle, Benoît Valiron, Formalization of a Programming Language for Quantum Circuits with Measurement and Classical Control, talk at Journées Informatique Quantique 2019 (Nov 2019) [[pdf](https://quantcert.github.io/GT-IQ%2719/slides/Lee.pdf), pdf]

• Dongho Lee, Valentin Perrelle, Benoît Valiron, Zhaowei Xu, Concrete Categorical Model of a Quantum Circuit Description Language with Measurement, Leibniz International Proceedings in Informatics 213 (2021) 51:1-51:20 [[arXiv:2110.02691](https://arxiv.org/abs/2110.02691), doi:10.4230/LIPIcs.FSTTCS.2021.51]

• Andrea Colledan, Ugo Dal Lago, On Dynamic Lifting and Effect Typing in Circuit Description Languages [[arXiv:2202.07636](https://arxiv.org/abs/2202.07636)]

• Andrea Colledan, Ugo Dal Lago, On Dynamic Lifting and Effect Typing in Circuit Description Languages, talk at TYPES Workshop, Nantes (2022) [[pdf](https://types22.inria.fr/files/2022/06/TYPES_2022_slides_13.pdf), pdf]

• Peng Fu, Kohei Kishida, Neil J. Ross, Peter Selinger, A biset-enriched categorical model for Proto-Quipper with dynamic lifting, in proceedings of Quantum Physics and Logic 2022 [[arXiv:2204.13039](https://arxiv.org/abs/2204.13039)]

• Peng Fu, Kohei Kishida, Neil J. Ross, Peter Selinger, Proto-Quipper with dynamic lifting, in proceedings of Quantum Physics and Logic 2022 [[arXiv:2204.13041](https://arxiv.org/abs/2204.13041)]

• Dongho Lee, Formal Methods for Quantum Programming Languages, Paris Saclay (Dec 2022) [[hal:tel-03895847](https://hal.science/LMF/tel-03895847)]