A tutorial introduction to quantum circuit programming in dependently typed Proto-Quipper
arXiv:2005.08396 · doi:10.1007/978-3-030-52482-1_9
Abstract
We introduce dependently typed Proto-Quipper, or Proto-Quipper-D for short, an experimental quantum circuit programming language with linear dependent types. We give several examples to illustrate how linear dependent types can help in the construction of correct quantum circuits. Specifically, we show how dependent types enable programming families of circuits, and how dependent types solve the problem of type-safe uncomputation of garbage qubits. We also discuss other language features along the way.
arXiv commentAdded a section on related work and a paragraph explaining qubit initialization and termination
References in corpus (9)
- Supplementary information for "Quantum supremacy using a programmable superconducting processor"
- Programmable Quantum Simulations of Spin Systems with Trapped Ions
- Exponential algorithmic speedup by quantum walk
- ProjectQ: An Open Source Software Framework for Quantum Computing
- Q#: Enabling scalable quantum computing and development with a high-level domain-specific language
- Quipper: A Scalable Quantum Programming Language
- An Introduction to Quantum Programming in Quipper
- A Categorical Model for a Quantum Circuit Description Language (Extended Abstract)
- Linear Dependent Type Theory for Quantum Programming Languages
Cited by in corpus (6)
- Integration of Quantum Accelerators with High Performance Computing -- A Review of Quantum Programming Tools
- Linear Dependent Type Theory for Quantum Programming Languages
- A Biset-Enriched Categorical Model for Proto-Quipper with Dynamic Lifting
- Qurts: Automatic Quantum Uncomputation by Affine Types with Lifetime
- Proto-Quipper with Reversing and Control
- Encoding High-level Quantum Programs as SZX-diagrams